1 /-
2 Copyright (c) 2017 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Mario Carneiro
5 -/
6 import tactic.basic
src └──────────┘
7 import data.list.basic data.stream data.lazy_list data.seq.computation logic.basic
src └─────────────┘ └─────────┘ └────────────┘ └──────────────────┘ └─────────┘
8
9 universes u v w
10
11 /-
12 coinductive seq (α : Type u) : Type u
13 | nil : seq α
14 | cons : α → seq α → seq α
15 -/
16
17 /--
18 A stream `s : option α` is a sequence if `s.nth n = none` implies `s.nth (n + 1) = none`.
19 -/
20 def stream.is_seq {α : Type u} (s : stream (option α)) : Prop :=
id └────┘ └────┘ ┴
src └────┘ └────┘
typ └────┘ └────┘ ┴
21 ∀ {n : ℕ}, s n = none → s (n + 1) = none
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘
src ┴ ┴ └──┘ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘
22
23 /-- `seq α` is the type of possibly infinite lists (referred here as sequences).
24 It is encoded as an infinite stream of options such that if `f n = none`, then
25 `f m = none` for all `m ≥ n`. -/
26 def seq (α : Type u) : Type u := { f : stream (option α) // f.is_seq }
id ┴ └────┘ └────┘ ┴ ┴└─────┘
src ┴ └────┘ └────┘ └─────┘
typ ┴ └────┘ └────┘ ┴ ┴└─────┘
doc └─────┘
27
28 /-- `seq1 α` is the type of nonempty sequences. -/
29 def seq1 (α) := α × seq α
id ┴ ┴ └─┘ ┴
src ┴ └─┘
typ ┴ ┴ └─┘ ┴
doc └─┘
30
31 namespace seq
32 variables {α : Type u} {β : Type v} {γ : Type w}
33
34 /-- The empty sequence -/
35 def nil : seq α := ⟨stream.const none, λn h, rfl⟩
id └─┘ ┴ └──────────┘ └──┘ ┴ ┴ └─┘
src └─┘ └──────────┘ └──┘ └─┘
typ └─┘ ┴ └──────────┘ └──┘ ┴ ┴ └─┘
doc └─┘
36
37 instance : inhabited (seq α) := ⟨nil⟩
id └───────┘ └─┘ ┴ └─┘
src └───────┘ └─┘ └─┘
typ └───────┘ └─┘ ┴ └─┘
doc └─┘ └─┘
38
39 /-- Prepend an element to a sequence -/
40 def cons (a : α) : seq α → seq α
id ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
41 | ⟨f, al⟩ := ⟨some a :: f, λn h, by {cases n with n, contradiction, exact al h}⟩
id ┴ └──┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴
src └──┘ └┘ └────┘ └─────┘ └───────────┘ └────┘ ┴
typ ┴ └──┘ ┴ └┘ ┴ ┴ └────┘┴└─────┘ └───────────┘ └────┘└┘┴┴
doc └────┘ └─────┘ └───────────┘ └────┘ ┴
txt └────┘ └─────┘ └───────────┘ └────┘ ┴
par └────┘ └─────┘ └───────────┘ └────┘ ┴
pid ┴ └─────┘ ┴ ┴
st └──────────────┘└─────────────┘└──────────┘└┘
42
43 /-- Get the nth element of a sequence (if it exists) -/
44 def nth : seq α → ℕ → option α := subtype.val
id └─┘ ┴ ┴ └────┘ ┴ └─────────┘
src └─┘ ┴ └────┘ └─────────┘
typ └─┘ ┴ ┴ └────┘ ┴ └─────────┘
doc └─┘
45
46 /-- A sequence has terminated at position `n` if the value at position `n` equals `none`. -/
47 def terminated_at (s : seq α) (n : ℕ) : Prop := s.nth n = none
id └─┘ ┴ ┴ ┴└──┘ ┴ ┴ └──┘
src └─┘ ┴ └──┘ ┴ └──┘
typ └─┘ ┴ ┴ ┴└──┘ ┴ ┴ └──┘
doc └─┘ └──┘
48
49 /-- It is decidable whether a sequence terminates at a given position. -/
50 instance terminated_at_decidable (s : seq α) (n : ℕ) : decidable (s.terminated_at n) :=
id └─┘ ┴ ┴ └───────┘ ┴└────────────┘ ┴
src └─┘ ┴ └───────┘ └────────────┘
typ └─┘ ┴ ┴ └───────┘ ┴└────────────┘ ┴
doc └─┘ └────────────┘
51 if p : s.nth n = none then is_true p
id └┘ ┴└──┘ ┴ ┴ └──┘ └─────┘ ┴
src └┘ └──┘ ┴ └──┘ └─────┘
typ └┘ ┴└──┘ ┴ ┴ └──┘ └─────┘ ┴
doc └──┘
52 else is_false (assume h, by contradiction)
id └──────┘ ┴
src └──────┘ └───────────┘
typ └──────┘ ┴ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
st └────────────┘
53
54 /-- A sequence terminates if there is some position `n` at which it has terminated. -/
55 def terminates (s : seq α) : Prop := ∃ (n : ℕ), s.terminated_at n
id └─┘ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴
src └─┘ ┴ ┴ ┴ └────────────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴
doc └─┘ └────────────┘
56
57 /-- Functorial action of the functor `option (α × _)` -/
58 @[simp] def omap (f : β → γ) : option (α × β) → option (α × γ)
id ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘ ┴ └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └──┘
59 | none := none
id └──┘ └──┘
src └──┘ └──┘
typ └──┘ └──┘
60 | (some (a, b)) := some (a, f b)
id └──┘ ┴┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ └──┘ ┴
typ └──┘ ┴┴ ┴ └──┘ ┴ ┴
61
62 /-- Get the first element of a sequence -/
63 def head (s : seq α) : option α := nth s 0
id └─┘ ┴ └────┘ ┴ └─┘ ┴
src └─┘ └────┘ └─┘
typ └─┘ ┴ └────┘ ┴ └─┘ ┴
doc └─┘ └─┘
64
65 /-- Get the tail of a sequence (or `nil` if the sequence is `nil`) -/
66 def tail : seq α → seq α
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
67 | ⟨f, al⟩ := ⟨f.tail, λ n, al⟩
id ┴ └┘ └───┘ ┴
src └───┘
typ ┴ └┘ └───┘ ┴
68
69 protected def mem (a : α) (s : seq α) := some a ∈ s.1
id ┴ └─┘ ┴ └──┘ ┴ ┴ ┴┴
src └─┘ └──┘ ┴ ┴
typ ┴ └─┘ ┴ └──┘ ┴ ┴ ┴┴
doc └─┘
70
71 instance : has_mem α (seq α) :=
id └─────┘ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ └─┘ ┴
doc └─┘
72 ⟨seq.mem⟩
id └─────┘
src └─────┘
typ └─────┘
73
74 theorem le_stable (s : seq α) {m n} (h : m ≤ n) :
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴
doc └─┘
75 s.1 m = none → s.1 n = none :=
id ┴┴ ┴ ┴ └──┘ ┴┴ ┴ ┴ └──┘
src ┴ ┴ └──┘ ┴ ┴ └──┘
typ ┴┴ ┴ ┴ └──┘ ┴┴ ┴ ┴ └──┘
76 by {cases s with f al, induction h with n h IH, exacts [id, λ h2, al (IH h2)]}
id ┴ ┴ └┘ └┘ └┘
src └────┘ └────────┘ └────────┘ └──────────┘ └──────┘└┘└┘ └───┘ ┴ ┴ └┘
typ └────┘┴└────────┘ └────────┘┴└──────────┘ └──────┘└┘└┘ └───┘└┘┴ └┘┴ └┘
doc └────┘ └────────┘ └────────┘ └──────────┘ └──────┘ └┘ └───┘ ┴ ┴ └┘
txt └────┘ └────────┘ └────────┘ └──────────┘ └──────┘ └┘ └───┘ ┴ ┴ └┘
par └────┘ └────────┘ └────────┘ └──────────┘ └──────┘ └┘ └───┘ ┴ ┴ └┘
pid ┴ └────────┘ ┴ ┴└─────────┘ └┘ └┘ └───┘ ┴ ┴ └┘
st └─────────────────┘└───────────────────────┘└─────────────────────────────┘└┘
77
78 /-- If a sequence terminated at position `n`, it also terminated at `m ≥ n `. -/
79 lemma terminated_stable {s : seq α} {m n : ℕ} (m_le_n : m ≤ n)
id └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴
doc └─┘
80 (terminated_at_m : s.terminated_at m) :
id ┴└────────────┘ ┴
src └────────────┘
typ ┴└────────────┘ ┴
doc └────────────┘
81 s.terminated_at n :=
id ┴└────────────┘ ┴
src └────────────┘
typ ┴└────────────┘ ┴
doc └────────────┘
82 le_stable s m_le_n terminated_at_m
id └───────┘ ┴ └────┘ └─────────────┘
src └───────┘
typ └───────┘ ┴ └────┘ └─────────────┘
83
84 /--
85 If `s.nth n = some aₙ` for some value `aₙ`, then there is also some value `aₘ` such
86 that `s.nth = some aₘ` for `m ≤ n`.
87 -/
88 lemma ge_stable (s : seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n)
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
89 (s_nth_eq_some : s.nth n = some aₙ) :
id ┴└──┘ ┴ ┴ └──┘ └┘
src └──┘ ┴ └──┘
typ ┴└──┘ ┴ ┴ └──┘ └┘
doc └──┘
90 ∃ (aₘ : α), s.nth m = some aₘ :=
id ┴ ┴ ┴ ┴└──┘ ┴ ┴ └──┘ └┘
src ┴ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ ┴└──┘ ┴ ┴ └──┘ └┘
doc └──┘
91 have s.nth n ≠ none, by simp [s_nth_eq_some],
id ┴└──┘ ┴ ┴ └──┘ └───────────┘
src └──┘ ┴ └──┘ └────┘ ┴
typ ┴└──┘ ┴ ┴ └──┘ └────┘└───────────┘┴
doc └──┘ └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────────┘
92 have s.nth m ≠ none, from mt (s.le_stable m_le_n) this,
id ┴└──┘ ┴ ┴ └──┘ └┘ ┴└────────┘ └────┘ └──┘
src └──┘ ┴ └──┘ └┘ └────────┘
typ ┴└──┘ ┴ ┴ └──┘ └┘ ┴└────────┘ └────┘ └──┘
doc └──┘
93 with_one.ne_one_iff_exists.elim_left this
id └────────────────────────┘└────────┘ └──┘
src └────────────────────────┘└────────┘
typ └────────────────────────┘└────────┘ └──┘
94
95 theorem not_mem_nil (a : α) : a ∉ @nil α :=
id ┴ ┴ ┴ └─┘ ┴
src ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴
doc └─┘
96 λ ⟨n, (h : some a = none)⟩, by injection h
id ┴ └──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘ └────────┘ └
typ ┴ └──┘ ┴ ┴ └──┘ └────────┘┴└
doc └────────┘ └
txt └────────┘ └
par └────────┘ └
pid ┴ └
st └────────────
97
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
98 theorem mem_cons (a : α) : ∀ (s : seq α), a ∈ cons a s
id ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └─┘ ┴ └──┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴
doc └─┘ └──┘
99 | ⟨f, al⟩ := stream.mem_cons (some a) _
id └─────────────┘ └──┘ ┴
src └─────────────┘ └──┘
typ └─────────────┘ └──┘ ┴
100
101 theorem mem_cons_of_mem (y : α) {a : α} : ∀ {s : seq α}, a ∈ s → a ∈ cons y s
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └─┘ ┴ ┴ └──┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └─┘ └──┘
102 | ⟨f, al⟩ := stream.mem_cons_of_mem (some y)
id └────────────────────┘ └──┘ ┴
src └────────────────────┘ └──┘
typ └────────────────────┘ └──┘ ┴
103
104 theorem eq_or_mem_of_mem_cons {a b : α} : ∀ {s : seq α}, a ∈ cons b s → a = b ∨ a ∈ s
id ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └──┘
105 | ⟨f, al⟩ h := (stream.eq_or_mem_of_mem_cons h).imp_left (λh, by injection h)
id ┴ └──────────────────────────┘ └──────┘ ┴ ┴
src └──────────────────────────┘ └──────┘ └────────┘
typ ┴ └──────────────────────────┘ └──────┘ ┴ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st └──────────┘
106
107 @[simp] theorem mem_cons_iff {a b : α} {s : seq α} : a ∈ cons b s ↔ a = b ∨ a ∈ s :=
id ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─┘ └──┘
108 ⟨eq_or_mem_of_mem_cons, λo, by cases o with e m;
id └───────────────────┘ ┴ ┴
src └───────────────────┘ └────┘ └───────┘
typ └───────────────────┘ ┴ └────┘┴└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st └──────────────────
109 [{rw e, apply mem_cons}, exact mem_cons_of_mem _ m]⟩
id ┴ ┴ └──────┘ └─────────────┘ ┴
src ┴ └─┘ └────┘└──────┘ └────┘└─────────────┘└─┘
typ ┴ └─┘┴ └────┘└──────┘ └────┘└─────────────┘└─┘┴
doc └─┘ └────┘ └────┘ └─┘
txt └─┘ └────┘ └────┘ └─┘
par └─┘ └────┘ └────┘ └─┘
pid ┴ ┴ ┴ └─┘
st ──┘└───┘└──────────────┘└┘└─────────────────────────┘
110
111 /-- Destructor for a sequence, resulting in either `none` (for `nil`) or
112 `some (a, s)` (for `cons a s`). -/
113 def destruct (s : seq α) : option (seq1 α) :=
id └─┘ ┴ └────┘ └──┘ ┴
src └─┘ └────┘ └──┘
typ └─┘ ┴ └────┘ └──┘ ┴
doc └─┘ └──┘
114 (λa', (a', s.tail)) <$> nth s 0
id └┘ ┴└┘ ┴└───┘ └─┘ └─┘ ┴
src ┴ └───┘ └─┘ └─┘
typ └┘ ┴└┘ ┴└───┘ └─┘ └─┘ ┴
doc └───┘ └─┘
115
116 theorem destruct_eq_nil {s : seq α} : destruct s = none → s = nil :=
id └─┘ ┴ └──────┘ ┴ ┴ └──┘ ┴ ┴ └─┘
src └─┘ └──────┘ ┴ └──┘ ┴ └─┘
typ └─┘ ┴ └──────┘ ┴ ┴ └──┘ ┴ ┴ └─┘
doc └─┘ └──────┘ └─┘
117 begin
st └─────
118 dsimp [destruct],
id └──────┘
src └─────┘└──────┘┴
typ └─────┘└──────┘┴
doc └─────┘└──────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────┘└─
119 induction f0 : nth s 0; intro h,
id └─┘ ┴
src └────────┘ └─┘└─┘┴ └┘ └─────┘
typ └────────┘ └─┘└─┘┴┴└┘ └─────┘
doc └────────┘ └─┘└─┘┴ └┘ └─────┘
txt └────────┘ └─┘ ┴ └┘ └─────┘
par └────────┘ └─┘ ┴ └┘ └─────┘
pid ┴ └─┘ ┴ ┴┴ └┘
st ────────────────────────────────┘└─
120 { apply subtype.eq,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└──────────────┘└─
121 funext n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └┘
st ───────────┘└─
122 induction n with n IH, exacts [f0, s.2 IH] },
id ┴ └┘ ┴ └┘
src └────────┘ └────────┘ └──────┘ └┘ └─┘ └┘
typ └────────┘┴└────────┘ └──────┘└┘└┘┴└─┘└┘└┘
doc └────────┘ └────────┘ └──────┘ └┘ └─┘ └┘
txt └────────┘ └────────┘ └──────┘ └┘ └─┘ └┘
par └────────┘ └────────┘ └──────┘ └┘ └─┘ └┘
pid ┴ ┴└───────┘ └┘ └┘ └─┘ ┴┴
st ────────────────────────┘└────────────────────┘└┘└
123 { contradiction }
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ─────────────────┘└─
124 end
st ──┘
125
126 theorem destruct_eq_cons {s : seq α} {a s'} : destruct s = some (a, s') → s = cons a s' :=
id └─┘ ┴ └──────┘ ┴ ┴ └──┘ ┴┴ └┘ ┴ ┴ └──┘ ┴ └┘
src └─┘ └──────┘ ┴ └──┘ ┴ ┴ └──┘
typ └─┘ ┴ └──────┘ ┴ ┴ └──┘ ┴┴ └┘ ┴ ┴ └──┘ ┴ └┘
doc └─┘ └──────┘ └──┘
127 begin
st └─────
128 dsimp [destruct],
id └──────┘
src └─────┘└──────┘┴
typ └─────┘└──────┘┴
doc └─────┘└──────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────┘└─
129 induction f0 : nth s 0 with a'; intro h,
id └─┘ ┴
src └────────┘ └─┘└─┘┴ └────────┘ └─────┘
typ └────────┘ └─┘└─┘┴┴└────────┘ └─────┘
doc └────────┘ └─┘└─┘┴ └────────┘ └─────┘
txt └────────┘ └─┘ ┴ └────────┘ └─────┘
par └────────┘ └─┘ ┴ └────────┘ └─────┘
pid ┴ └─┘ ┴ ┴└┘└─────┘ └┘
st ────────────────────────────────────────┘└─
130 { contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───┘└────────────┘└┘└
131 { unfold functor.map at h,
src └─────────────────────┘
typ └─────────────────────┘
doc └─────────────────────┘
txt └─────────────────────┘
par └─────────────────────┘
pid └──────────┘└───┘
st ──────────────────────────┘└─
132 cases s with f al,
id ┴
src └────┘ └────────┘
typ └────┘┴└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ────────────────────┘└─
133 injections with _ h1 h2,
src └─────────────────────┘
typ └─────────────────────┘
doc └─────────────────────┘
txt └─────────────────────┘
par └─────────────────────┘
pid └───────────┘
st ──────────────────────────┘└─
134 rw ←h2, apply subtype.eq, dsimp [tail, cons],
id └┘ └────────┘ └──┘ └──┘
src └──┘ └────┘└────────┘ └─────┘└──┘└┘└──┘┴
typ └──┘└┘ └────┘└────────┘ └─────┘└──┘└┘└──┘┴
doc └──┘ └────┘ └─────┘└──┘└┘└──┘┴
txt └──┘ └────┘ └─────┘ └┘ ┴
par └──┘ └────┘ └─────┘ └┘ ┴
pid └┘ ┴ ┴┴ └┘ ┴
st ─────────┘└────────────────┘└──────────────────┘└─
135 rw h1 at f0, rw ←f0,
id └┘ └┘
src └─┘ └────┘ └──┘
typ └─┘└┘└────┘ └──┘└┘
doc └─┘ └────┘ └──┘
txt └─┘ └────┘ └──┘
par └─┘ └────┘ └──┘
pid ┴ └────┘ └┘
st ──────────────┘└──────┘└─
136 exact (stream.eta f).symm }
id └────────┘ ┴
src └────┘ └────────┘┴ └─────┘
typ └────┘ └────────┘┴┴└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └───┘└┘
st ─────────────────────────────┘└─
137 end
st ──┘
138
139 @[simp] theorem destruct_nil : destruct (nil : seq α) = none := rfl
id └──────┘ └─┘ └─┘ ┴ ┴ └──┘ └─┘
src └──────┘ └─┘ └─┘ ┴ └──┘ └─┘
typ └──────┘ └─┘ └─┘ ┴ ┴ └──┘ └─┘
doc └──┘ └──────┘ └─┘ └─┘
140
141 @[simp] theorem destruct_cons (a : α) : ∀ s, destruct (cons a s) = some (a, s)
id ┴ ┴ └──────┘ └──┘ ┴ ┴ ┴ └──┘ ┴┴ ┴
src └──────┘ └──┘ ┴ └──┘ ┴
typ ┴ ┴ └──────┘ └──┘ ┴ ┴ ┴ └──┘ ┴┴ ┴
doc └──┘ └──────┘ └──┘
142 | ⟨f, al⟩ := begin
st └─────
143 unfold cons destruct functor.map,
src └──────────────────────────────┘
typ └──────────────────────────────┘
doc └──────────────────────────────┘
txt └──────────────────────────────┘
par └──────────────────────────────┘
pid └────────────────────────┘
st ─────────────────────────────────┘└─
144 apply congr_arg (λ s, some (a, s)),
id └───────┘ └──┘ ┴┴
src └────┘└───────┘┴ └──┘└──┘┴┴ └┘ └┘
typ └────┘└───────┘┴ └──┘└──┘┴┴┴└┘ └┘
doc └────┘ ┴ └──┘ ┴ └┘ └┘
txt └────┘ ┴ └──┘ ┴ └┘ └┘
par └────┘ ┴ └──┘ ┴ └┘ └┘
pid ┴ ┴ └──┘ ┴ └┘ └┘
st ───────────────────────────────────┘└─
145 apply subtype.eq, dsimp [tail], rw [stream.tail_cons]
id └────────┘ └──┘ └──────────────┘
src └────┘└────────┘ └─────┘└──┘┴ └──┘└──────────────┘└┘
typ └────┘└────────┘ └─────┘└──┘┴ └──┘└──────────────┘└┘
doc └────┘ └─────┘└──┘┴ └──┘ └┘
txt └────┘ └─────┘ ┴ └──┘ └┘
par └────┘ └─────┘ ┴ └──┘ └┘
pid ┴ ┴┴ ┴ └┘ ┴┴
st ─────────────────┘└────────────┘└────────────────────┘┴┴
146 end
st └─┘
147
148 theorem head_eq_destruct (s : seq α) : head s = prod.fst <$> destruct s :=
id └─┘ ┴ └──┘ ┴ ┴ └──────┘ └─┘ └──────┘ ┴
src └─┘ └──┘ ┴ └──────┘ └─┘ └──────┘
typ └─┘ ┴ └──┘ ┴ ┴ └──────┘ └─┘ └──────┘ ┴
doc └─┘ └──┘ └──────┘
149 by unfold destruct head; cases nth s 0; refl
id └─┘ ┴
src └──────────────────┘ └────┘└─┘┴ └┘ └────
typ └──────────────────┘ └────┘└─┘┴┴└┘ └────
doc └──────────────────┘ └────┘└─┘┴ └┘ └────
txt └──────────────────┘ └────┘ ┴ └┘ └────
par └──────────────────┘ └────┘ ┴ └┘ └────
pid └────────────┘ ┴ ┴ ┴┴ └
st └──────────────────────────────────────────
150
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
151 @[simp] theorem head_nil : head (nil : seq α) = none := rfl
id └──┘ └─┘ └─┘ ┴ ┴ └──┘ └─┘
src └──┘ └─┘ └─┘ ┴ └──┘ └─┘
typ └──┘ └─┘ └─┘ ┴ ┴ └──┘ └─┘
doc └──┘ └──┘ └─┘ └─┘
152
153 @[simp] theorem head_cons (a : α) (s) : head (cons a s) = some a :=
id ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘ ┴
src └──┘ └──┘ ┴ └──┘
typ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘
154 by rw [head_eq_destruct, destruct_cons]; refl
id └──────────────┘ └───────────┘
src └──┘└──────────────┘└┘└───────────┘┴ └────
typ └──┘└──────────────┘└┘└───────────┘┴ └────
doc └──┘ └┘ ┴ └────
txt └──┘ └┘ ┴ └────
par └──┘ └┘ ┴ └────
pid └┘ └┘ ┴ └
st └───────────────────┘└─────────────┘┴└──────
155
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
156 @[simp] theorem tail_nil : tail (nil : seq α) = nil := rfl
id └──┘ └─┘ └─┘ ┴ ┴ └─┘ └─┘
src └──┘ └─┘ └─┘ ┴ └─┘ └─┘
typ └──┘ └─┘ └─┘ ┴ ┴ └─┘ └─┘
doc └──┘ └──┘ └─┘ └─┘ └─┘
157
158 @[simp] theorem tail_cons (a : α) (s) : tail (cons a s) = s :=
id ┴ └──┘ └──┘ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴
typ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
159 by cases s with f al; apply subtype.eq; dsimp [tail, cons]; rw [stream.tail_cons]
id ┴ └────────┘ └──┘ └──┘ └──────────────┘
src └────┘ └────────┘ └────┘└────────┘ └─────┘└──┘└┘└──┘┴ └──┘└──────────────┘└─
typ └────┘┴└────────┘ └────┘└────────┘ └─────┘└──┘└┘└──┘┴ └──┘└──────────────┘└─
doc └────┘ └────────┘ └────┘ └─────┘└──┘└┘└──┘┴ └──┘ └─
txt └────┘ └────────┘ └────┘ └─────┘ └┘ ┴ └──┘ └─
par └────┘ └────────┘ └────┘ └─────┘ └┘ ┴ └──┘ └─
pid ┴ └────────┘ ┴ ┴┴ └┘ ┴ └┘ ┴└
st └────────────────────────────────────────────────────────────┘└──────────────┘┴└
160
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
161 def cases_on {C : seq α → Sort v} (s : seq α)
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
doc └─┘ └─┘
162 (h1 : C nil) (h2 : ∀ x s, C (cons x s)) : C s := begin
id ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └─┘ └──┘
typ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └─┘ └──┘
st └─────
163 induction H : destruct s with v v,
id └──────┘ ┴
src └────────┘ └─┘└──────┘┴ └───────┘
typ └────────┘ └─┘└──────┘┴┴└───────┘
doc └────────┘ └─┘└──────┘┴ └───────┘
txt └────────┘ └─┘ ┴ └───────┘
par └────────┘ └─┘ ┴ └───────┘
pid ┴ └─┘ ┴ ┴└──────┘
st ──────────────────────────────────┘└─
164 { rw destruct_eq_nil H, apply h1 },
id └─────────────┘ ┴
src └─┘└─────────────┘┴ └────┘ ┴
typ └─┘└─────────────┘┴┴ └────┘ ┴
doc └─┘ ┴ └────┘ ┴
txt └─┘ ┴ └────┘ ┴
par └─┘ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ───┘└──────────────────┘└─────────┘└┘└
165 { cases v with a s', rw destruct_eq_cons H, apply h2 }
id ┴ └──────────────┘ ┴
src └────┘ └────────┘ └─┘└──────────────┘┴ └────┘ ┴
typ └────┘┴└────────┘ └─┘└──────────────┘┴┴ └────┘ ┴
doc └────┘ └────────┘ └─┘ ┴ └────┘ ┴
txt └────┘ └────────┘ └─┘ ┴ └────┘ ┴
par └────┘ └────────┘ └─┘ ┴ └────┘ ┴
pid ┴ └────────┘ ┴ ┴ ┴ ┴
st ────────────────────┘└─────────────────────┘└─────────┘└─
166 end
st ──┘
167
168 theorem mem_rec_on {C : seq α → Prop} {a s} (M : a ∈ s)
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴
doc └─┘
169 (h1 : ∀ b s', (a = b ∨ C s') → C (cons b s')) : C s :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ └┘ ┴ ┴
src ┴ ┴ └──┘
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ └┘ ┴ ┴
doc └──┘
170 begin
st └─────
171 cases M with k e, unfold stream.nth at e,
id ┴
src └────┘ └───────┘ └────────────────────┘
typ └────┘┴└───────┘ └────────────────────┘
doc └────┘ └───────┘ └────────────────────┘
txt └────┘ └───────┘ └────────────────────┘
par └────┘ └───────┘ └────────────────────┘
pid ┴ └───────┘ └─────────┘└───┘
st ─────────────────┘└──────────────────────┘└─
172 induction k with k IH generalizing s,
id ┴
src └────────┘ └───────────────────────┘
typ └────────┘┴└───────────────────────┘
doc └────────┘ └───────────────────────┘
txt └────────┘ └───────────────────────┘
par └────────┘ └───────────────────────┘
pid ┴ ┴└───────┘└─────────────┘
st ─────────────────────────────────────┘└─
173 { have TH : s = cons a (tail s),
id ┴ └──┘ ┴ └──┘ ┴
src └────────┘ ┴┴┴└──┘┴ ┴ └──┘┴ ┴
typ └────────┘ ┴┴┴└──┘┴┴┴ └──┘┴┴┴
doc └────────┘ ┴ ┴└──┘┴ ┴ └──┘┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───┘└───────────────────────────┘└─
174 { apply destruct_eq_cons,
id └──────────────┘
src └────┘└──────────────┘
typ └────┘└──────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└────────────────────┘└─
175 unfold destruct nth functor.map, rw ←e, refl },
id ┴
src └─────────────────────────────┘ └──┘ └───┘
typ └─────────────────────────────┘ └──┘┴ └───┘
doc └─────────────────────────────┘ └──┘ └───┘
txt └─────────────────────────────┘ └──┘ └───┘
par └─────────────────────────────┘ └──┘ └───┘
pid └───────────────────────┘ └┘ ┴
st ────────────────────────────────────┘└─────┘└─────┘└┘└
176 rw TH, apply h1 _ _ (or.inl rfl) },
id └┘ └┘ └────┘ └─┘
src └─┘ └────┘ └───┘ └────┘┴└─┘└┘
typ └─┘└┘ └────┘└┘└───┘ └────┘┴└─┘└┘
doc └─┘ └────┘ └───┘ ┴ └┘
txt └─┘ └────┘ └───┘ ┴ └┘
par └─┘ └────┘ └───┘ ┴ └┘
pid ┴ ┴ └───┘ ┴ ┴┴
st ────────┘└──────────────────────────┘└┘└
177 revert e, apply s.cases_on _ (λ b s', _); intro e,
id └────────┘
src └──────┘ └────┘└────────┘└─┘ └───────┘ └─────┘
typ └──────┘ └────┘└────────┘└─┘ └───────┘ └─────┘
doc └──────┘ └────┘ └─┘ └───────┘ └─────┘
txt └──────┘ └────┘ └─┘ └───────┘ └─────┘
par └──────┘ └────┘ └─┘ └───────┘ └─────┘
pid └┘ ┴ └─┘ └───────┘ └┘
st ─────────┘└───────────────────────────────────────┘└─
178 { injection e },
id ┴
src └────────┘ ┴
typ └────────┘┴┴
doc └────────┘ ┴
txt └────────┘ ┴
par └────────┘ ┴
pid ┴ ┴
st ───┘└──────────┘└┘└
179 { have h_eq : (cons b s').val (nat.succ k) = s'.val k, { cases s'; refl },
id └──┘ ┴ └──────┘ └────┘ ┴ └┘
src └──────────┘ └──┘┴ ┴ └────┘ └──────┘┴ └┘ ┴└────┘┴ └────┘ └───┘
typ └──────────┘ └──┘┴┴┴ └────┘ └──────┘┴ └┘ ┴└────┘┴┴ └────┘└┘ └───┘
doc └──────────┘ └──┘┴ ┴ └────┘ ┴ └┘ ┴ ┴ └────┘ └───┘
txt └──────────┘ ┴ ┴ └────┘ ┴ └┘ ┴ ┴ └────┘ └───┘
par └──────────┘ ┴ ┴ └────┘ ┴ └┘ ┴ ┴ └────┘ └───┘
pid └───────┘└─┘ ┴ ┴ └────┘ ┴ └┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────┘└──┘└─────────────┘└┘└
180 rw [h_eq] at e,
id └──┘
src └──┘ └────┘
typ └──┘└──┘└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid └┘ ┴└───┘
st ───────────┘┴└───┘└─
181 apply h1 _ _ (or.inr (IH e)) }
id └┘ └────┘ └┘ ┴
src └────┘ └───┘ └────┘┴ ┴ └─┘
typ └────┘└┘└───┘ └────┘┴ └┘┴┴└─┘
doc └────┘ └───┘ ┴ ┴ └─┘
txt └────┘ └───┘ ┴ ┴ └─┘
par └────┘ └───┘ ┴ ┴ └─┘
pid ┴ └───┘ ┴ ┴ └┘┴
st ────────────────────────────────┘└─
182 end
st ──┘
183
184 def corec.F (f : β → option (α × β)) : option β → option α × option β
id ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
src └────┘ ┴ └────┘ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
185 | none := (none, none)
id └──┘ ┴└──┘ └──┘
src └──┘ ┴└──┘ └──┘
typ └──┘ ┴└──┘ └──┘
186 | (some b) := match f b with none := (none, none) | some (a, b') := (some a, some b') end
id └──┘ ┴ ┴ └──┘ ┴└──┘ └──┘ └──┘ ┴┴ └┘ ┴└──┘ └──┘
src └──┘ └──┘ ┴└──┘ └──┘ └──┘ ┴ ┴└──┘ └──┘
typ └──┘ ┴ ┴ └──┘ ┴└──┘ └──┘ └──┘ ┴┴ └┘ ┴└──┘ └──┘
187
188 /-- Corecursor for `seq α` as a coinductive type. Iterates `f` to produce new elements
189 of the sequence until `none` is obtained. -/
190 def corec (f : β → option (α × β)) (b : β) : seq α :=
id ┴ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └────┘ ┴ └─┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─┘
191 begin
st └─────
192 refine ⟨stream.corec' (corec.F f) (some b), λn h, _⟩,
id └───────────┘ └─────┘ ┴ └──┘ ┴
src └─────┘ └───────────┘┴ └─────┘┴ └┘ └──┘┴ └─┘ └─────┘
typ └─────┘ └───────────┘┴ └─────┘┴┴└┘ └──┘┴┴└─┘ └─────┘
doc └─────┘ ┴ ┴ └┘ ┴ └─┘ └─────┘
txt └─────┘ ┴ ┴ └┘ ┴ └─┘ └─────┘
par └─────┘ ┴ ┴ └┘ ┴ └─┘ └─────┘
pid ┴ ┴ ┴ └┘ ┴ └─┘ └─────┘
st ─────────────────────────────────────────────────────┘└─
193 rw stream.corec'_eq,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
194 change stream.corec' (corec.F f) (corec.F f (some b)).2 n = none,
id └───────────┘ └─────┘ ┴ └──┘ ┴ ┴ ┴ └──┘
src └─────┘└───────────┘┴ ┴ └┘ └─────┘┴ ┴ └──┘┴ └───┘ ┴┴┴└──┘
typ └─────┘└───────────┘┴ ┴ └┘ └─────┘┴┴┴ └──┘┴┴└───┘┴┴┴┴└──┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────┘└─
195 revert h, generalize : some b = o, revert o,
id └──┘ ┴
src └──────┘ └───────────┘└──┘┴ ┴ ┴ └──────┘
typ └──────┘ └───────────┘└──┘┴┴┴ ┴ └──────┘
doc └──────┘ └───────────┘ ┴ ┴ ┴ └──────┘
txt └──────┘ └───────────┘ ┴ ┴ ┴ └──────┘
par └──────┘ └───────────┘ ┴ ┴ ┴ └──────┘
pid └┘ ┴┴┴ ┴ ┴ ┴ └┘
st ─────────┘└───────────────────────┘└────────┘└─
196 induction n with n IH; intro o,
id ┴
src └────────┘ └────────┘ └─────┘
typ └────────┘┴└────────┘ └─────┘
doc └────────┘ └────────┘ └─────┘
txt └────────┘ └────────┘ └─────┘
par └────────┘ └────────┘ └─────┘
pid ┴ ┴└───────┘ └┘
st ───────────────────────────────┘└─
197 { change (corec.F f o).1 = none → (corec.F f (corec.F f o).2).1 = none,
id ┴ └─────┘ ┴ ┴ └──┘
src └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────┘┴ ┴ └─────┘ ┴└──┘
typ └─────┘ ┴ ┴ └──┘┴┴ ┴ ┴ ┴ ┴ └─────┘┴┴┴┴└─────┘ ┴└──┘
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
pid ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
st ───┘└──────────────────────────────────────────────────────────────────┘└─
198 cases o with b; intro h, { refl },
id ┴
src └────┘ └─────┘ └─────┘ └───┘
typ └────┘┴└─────┘ └─────┘ └───┘
doc └────┘ └─────┘ └─────┘ └───┘
txt └────┘ └─────┘ └─────┘ └───┘
par └────┘ └─────┘ └─────┘ └───┘
pid ┴ └─────┘ └┘ ┴
st ──────────────────────────┘└──┘└───┘└┘└
199 dsimp [corec.F] at h, dsimp [corec.F],
id └─────┘ └─────┘
src └─────┘└─────┘└────┘ └─────┘└─────┘┴
typ └─────┘└─────┘└────┘ └─────┘└─────┘┴
doc └─────┘ └────┘ └─────┘ ┴
txt └─────┘ └────┘ └─────┘ ┴
par └─────┘ └────┘ └─────┘ ┴
pid ┴┴ ┴┴└──┘ ┴┴ ┴
st ───────────────────────┘└───────────────┘└─
200 cases f b with s, { refl },
id ┴ ┴
src └────┘ ┴ └─────┘ └───┘
typ └────┘┴┴┴└─────┘ └───┘
doc └────┘ ┴ └─────┘ └───┘
txt └────┘ ┴ └─────┘ └───┘
par └────┘ ┴ └─────┘ └───┘
pid ┴ ┴ └─────┘ ┴
st ───────────────────┘└──┘└───┘└┘└
201 { cases s with a b', contradiction } },
id ┴
src └────┘ └────────┘ └────────────┘
typ └────┘┴└────────┘ └────────────┘
doc └────┘ └────────┘ └────────────┘
txt └────┘ └────────┘ └────────────┘
par └────┘ └────────┘ └────────────┘
pid ┴ └────────┘ ┴
st ──────────────────────┘└──────────────┘└──┘└
202 { rw [stream.corec'_eq (corec.F f) (corec.F f o).2,
id └──────────────┘ └─────┘ ┴ ┴
src └──┘└──────────────┘┴ ┴ └┘ └─────┘┴ ┴ └────
typ └──┘└──────────────┘┴ ┴ └┘ └─────┘┴┴┴┴└────
doc └──┘ ┴ ┴ └┘ ┴ ┴ └────
txt └──┘ ┴ ┴ └┘ ┴ ┴ └────
par └──┘ ┴ ┴ └┘ ┴ ┴ └────
pid └┘ ┴ ┴ └┘ ┴ ┴ └────
st ─────────────────────────────────────────────────┘└───
203 stream.corec'_eq (corec.F f) o],
id └──────────────┘ └─────┘ ┴ ┴
src ───────┘└──────────────┘┴ └─────┘┴ └┘ ┴
typ ───────┘└──────────────┘┴ └─────┘┴┴└┘┴┴
doc ───────┘ ┴ ┴ └┘ ┴
txt ───────┘ ┴ ┴ └┘ ┴
par ───────┘ ┴ ┴ └┘ ┴
pid ───────┘ ┴ ┴ └┘ ┴
st ─────────────────────────────────────┘┴└─
204 exact IH (corec.F f o).2 }
id └┘ └─────┘ ┴ ┴
src └────┘ ┴ └─────┘┴ ┴ └──┘
typ └────┘└┘┴ └─────┘┴┴┴┴└──┘
doc └────┘ ┴ ┴ ┴ └──┘
txt └────┘ ┴ ┴ ┴ └──┘
par └────┘ ┴ ┴ ┴ └──┘
pid ┴ ┴ ┴ ┴ ┴└─┘
st ────────────────────────────┘└─
205 end
st ──┘
206
207 @[simp] theorem corec_eq (f : β → option (α × β)) (b : β) :
id ┴ └────┘ ┴ ┴ ┴ ┴
src └────┘ ┴
typ ┴ └────┘ ┴ ┴ ┴ ┴
doc └──┘
208 destruct (corec f b) = omap (corec f) (f b) :=
id └──────┘ └───┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
src └──────┘ └───┘ ┴ └──┘ └───┘
typ └──────┘ └───┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
doc └──────┘ └───┘ └──┘ └───┘
209 begin
st └─────
210 dsimp [corec, destruct, nth],
id └───┘ └──────┘ └─┘
src └─────┘└───┘└┘└──────┘└┘└─┘┴
typ └─────┘└───┘└┘└──────┘└┘└─┘┴
doc └─────┘└───┘└┘└──────┘└┘└─┘┴
txt └─────┘ └┘ └┘ ┴
par └─────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ─────────────────────────────┘└─
211 change stream.corec' (corec.F f) (some b) 0 with (corec.F f (some b)).1,
id └───────────┘ └─────┘ ┴ └──┘ ┴ └─────┘ ┴ └──┘ ┴
src └─────┘└───────────┘┴ └─────┘┴ └┘ └──┘┴ └───────┘ └─────┘┴ ┴ └──┘┴ └──┘
typ └─────┘└───────────┘┴ └─────┘┴┴└┘ └──┘┴┴└───────┘ └─────┘┴┴┴ └──┘┴┴└──┘
doc └─────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ ┴ ┴ └──┘
par └─────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ ┴ ┴ └──┘
pid ┴ ┴ ┴ └┘ ┴ └┘└─────┘ ┴ ┴ ┴ └┘└┘
st ────────────────────────────────────────────────────────────────────────┘└─
212 unfold functor.map, dsimp [corec.F],
id └─────┘
src └────────────────┘ └─────┘└─────┘┴
typ └────────────────┘ └─────┘└─────┘┴
doc └────────────────┘ └─────┘ ┴
txt └────────────────┘ └─────┘ ┴
par └────────────────┘ └─────┘ ┴
pid └──────────┘ ┴┴ ┴
st ───────────────────┘└───────────────┘└─
213 induction h : f b with s, { refl },
id ┴ ┴
src └────────┘ └─┘ ┴ └─────┘ └───┘
typ └────────┘ └─┘┴┴┴└─────┘ └───┘
doc └────────┘ └─┘ ┴ └─────┘ └───┘
txt └────────┘ └─┘ ┴ └─────┘ └───┘
par └────────┘ └─┘ ┴ └─────┘ └───┘
pid ┴ └─┘ ┴ ┴└────┘ ┴
st ─────────────────────────┘└──┘└───┘└┘└
214 cases s with a b', dsimp [corec.F],
id ┴ └─────┘
src └────┘ └────────┘ └─────┘└─────┘┴
typ └────┘┴└────────┘ └─────┘└─────┘┴
doc └────┘ └────────┘ └─────┘ ┴
txt └────┘ └────────┘ └─────┘ ┴
par └────┘ └────────┘ └─────┘ ┴
pid ┴ └────────┘ ┴┴ ┴
st ──────────────────┘└───────────────┘└─
215 apply congr_arg (λ b', some (a, b')),
id └───────┘ └──┘ ┴┴
src └────┘└───────┘┴ └───┘└──┘┴┴ └┘ └┘
typ └────┘└───────┘┴ └───┘└──┘┴┴┴└┘ └┘
doc └────┘ ┴ └───┘ ┴ └┘ └┘
txt └────┘ ┴ └───┘ ┴ └┘ └┘
par └────┘ ┴ └───┘ ┴ └┘ └┘
pid ┴ ┴ └───┘ ┴ └┘ └┘
st ─────────────────────────────────────┘└─
216 apply subtype.eq,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────┘└─
217 dsimp [corec, tail],
id └───┘ └──┘
src └─────┘└───┘└┘└──┘┴
typ └─────┘└───┘└┘└──┘┴
doc └─────┘└───┘└┘└──┘┴
txt └─────┘ └┘ ┴
par └─────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────┘└─
218 rw [stream.corec'_eq, stream.tail_cons],
id └──────────────┘ └──────────────┘
src └──┘└──────────────┘└┘└──────────────┘┴
typ └──┘└──────────────┘└┘└──────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────────┘└────────────────┘└──
219 dsimp [corec.F], rw h, refl
id └─────┘ ┴
src └─────┘└─────┘┴ └─┘ └───┘
typ └─────┘└─────┘┴ └─┘┴ └───┘
doc └─────┘ ┴ └─┘ └───┘
txt └─────┘ ┴ └─┘ └───┘
par └─────┘ ┴ └─┘ └───┘
pid ┴┴ ┴ ┴ ┴
st ────────────────┘└────┘└─────┘
220 end
st └─┘
221
222 /-- Embed a list as a sequence -/
223 def of_list (l : list α) : seq α :=
id └──┘ ┴ └─┘ ┴
src └──┘ └─┘
typ └──┘ ┴ └─┘ ┴
doc └─┘
224 ⟨list.nth l, λn h, begin
id └──────┘ ┴ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴ ┴
st └─────
225 induction l with a l IH generalizing n, refl,
id ┴
src └────────┘ └─────────────────────────┘ └──┘
typ └────────┘┴└─────────────────────────┘ └──┘
doc └────────┘ └─────────────────────────┘ └──┘
txt └────────┘ └─────────────────────────┘ └──┘
par └────────┘ └─────────────────────────┘ └──┘
pid ┴ ┴└─────────┘└─────────────┘
st ───────────────────────────────────────┘└────┘└─
226 dsimp [list.nth], cases n with n; dsimp [list.nth] at h,
id └──────┘ ┴ └──────┘
src └─────┘└──────┘┴ └────┘ └─────┘ └─────┘└──────┘└────┘
typ └─────┘└──────┘┴ └────┘┴└─────┘ └─────┘└──────┘└────┘
doc └─────┘ ┴ └────┘ └─────┘ └─────┘ └────┘
txt └─────┘ ┴ └────┘ └─────┘ └─────┘ └────┘
par └─────┘ ┴ └────┘ └─────┘ └─────┘ └────┘
pid ┴┴ ┴ ┴ └─────┘ ┴┴ ┴┴└──┘
st ─────────────────┘└─────────────────────────────────────┘└─
227 { contradiction },
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───┘└────────────┘└┘└
228 { apply IH _ h }
id └┘ ┴
src └────┘ └─┘ ┴
typ └────┘└┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────┘└─
229 end⟩
st ──┘
230
231 instance coe_list : has_coe (list α) (seq α) := ⟨of_list⟩
id └─────┘ └──┘ ┴ └─┘ ┴ └─────┘
src └─────┘ └──┘ └─┘ └─────┘
typ └─────┘ └──┘ ┴ └─┘ ┴ └─────┘
doc └─┘ └─────┘
232
233 section bisim
234 variable (R : seq α → seq α → Prop)
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
doc └─┘ └─┘
235
236 local infix ~ := R
237
238 def bisim_o : option (seq1 α) → option (seq1 α) → Prop
id └────┘ └──┘ ┴ ┴ └────┘ └──┘ ┴
src └────┘ └──┘ └────┘ └──┘
typ └────┘ └──┘ ┴ ┴ └────┘ └──┘ ┴
doc └──┘ └──┘
239 | none none := true
id └──┘ └──┘
src └──┘ └──┘
typ └──┘ └──┘
240 | (some (a, s)) (some (a', s')) := a = a' ∧ R s s'
id ┴┴ ┴ └──┘ ┴└┘ └┘ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴
typ ┴┴ ┴ └──┘ ┴└┘ └┘ ┴ ┴ ┴
241 | _ _ := false
id └───┘
src └───┘
typ └───┘
242 attribute [simp] bisim_o
id └─────┘
src └─────┘
typ └─────┘
doc └──┘
243
244 def is_bisimulation := ∀ ⦃s₁ s₂⦄, s₁ ~ s₂ → bisim_o R (destruct s₁) (destruct s₂)
id └┘ └┘ └┘ ┴ └┘ └─────┘ ┴ └──────┘ └┘ └──────┘ └┘
src └─────┘ └──────┘ └──────┘
typ └┘ └┘ └┘ ┴ └┘ └─────┘ ┴ └──────┘ └┘ └──────┘ └┘
doc └──────┘ └──────┘
245
246 -- If two streams are bisimilar, then they are equal
247 theorem eq_of_bisim (bisim : is_bisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂ :=
id └─────────────┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
src └─────────────┘ ┴
typ └─────────────┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
248 begin
st └─────
249 apply subtype.eq,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
250 apply stream.eq_of_bisim (λx y, ∃ s s' : seq α, s.1 = x ∧ s'.1 = y ∧ R s s'),
id └────────────────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴
src └────┘└────────────────┘┴ └───┘┴└──────┘└─┘┴ ┴┴ └─┘┴┴ ┴┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └────┘└────────────────┘┴ └───┘┴└──────┘└─┘┴┴┴┴ └─┘┴┴ ┴┴┴ └─┘ ┴ ┴ ┴┴┴ ┴ ┴
doc └────┘ ┴ └───┘ └──────┘└─┘┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ └───┘ └──────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ └───┘ └──────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ └───┘ └──────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────┘└─
251 dsimp [stream.is_bisimulation],
id └────────────────────┘
src └─────┘└────────────────────┘┴
typ └─────┘└────────────────────┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────────────────────┘└─
252 intros t₁ t₂ e,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ─────────────────┘└─
253 exact match t₁, t₂, e with ._, ._, ⟨s, s', rfl, rfl, r⟩ :=
id └┘ └┘ ┴ ┴ └┘ └─┘
src └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘└─┘└┘ └────
typ └────┘ ┴└┘└┘└┘└┘┴└────┘ └┘ └┘ ┴└┘└┘└┘ └┘└─┘└┘ └────
doc └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └────
txt └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └────
par └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └────
pid ┴ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └────
st ───────────────────────────────────────────────────────────────
254 suffices head s = head s' ∧ R (tail s) (tail s'), from
id └──┘ ┴
src ─────┘ └────┘ ┴ ┴└──┘┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
typ ─────┘ └────┘ ┴ ┴└──┘┴ ┴ ┴┴┴ ┴ └┘ ┴ └───────
doc ─────┘ └────┘ ┴ ┴└──┘┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
txt ─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
par ─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
pid ─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────
st ─────────────────────────────────────────────────────────────
255 and.imp id (λr, ⟨tail s, tail s',
id └─────┘ └┘ └──┘
src ─────┘└─────┘┴└┘┴ └─┘ ┴ └┘└──┘┴ └─
typ ─────┘└─────┘┴└┘┴ └─┘ ┴ └┘└──┘┴ └─
doc ─────┘ ┴ ┴ └─┘ ┴ └┘└──┘┴ └─
txt ─────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └─
par ─────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └─
pid ─────┘ ┴ ┴ └─┘ ┴ └┘ ┴ └─
st ────────────────────────────────────────
256 by cases s; refl, by cases s'; refl, r⟩) this,
id ┴ └┘
src ───────┘ ┴└────┘ └┘└──┘└┘ ┴└────┘ └┘└──┘└┘ └─┘ └─
typ ───────┘ ┴└────┘┴└┘└──┘└┘ ┴└────┘└┘└┘└──┘└┘ └─┘ └─
doc ───────┘ ┴└────┘ └┘└──┘└┘ ┴└────┘ └┘└──┘└┘ └─┘ └─
txt ───────┘ ┴└────┘ └┘└──┘└┘ ┴└────┘ └┘└──┘└┘ └─┘ └─
par ───────┘ ┴└────┘ └┘└──┘└┘ ┴└────┘ └┘└──┘└┘ └─┘ └─
pid ───────┘ └─────┘ └──────┘ └─────┘ └──────┘ └─┘ └─
st ─────────┘└────────────┘└──┘└─────────────┘└───────────
257 begin
src ─────┘ └
typ ─────┘ └
doc ─────┘ └
txt ─────┘ └
par ─────┘ └
pid ─────┘ └
st ─────┘└─────
258 have := bisim r, revert r this,
id └───┘ ┴
src ───────┘└──────┘ ┴ └┘└───────────┘└─
typ ───────┘└──────┘└───┘┴┴└┘└───────────┘└─
doc ───────┘└──────┘ ┴ └┘└───────────┘└─
txt ───────┘└──────┘ ┴ └┘└───────────┘└─
par ───────┘└──────┘ ┴ └┘└───────────┘└─
pid ───────────────┘ ┴ └────────────────
st ──────────────────────┘└─────────────┘└─
259 apply cases_on s _ _; intros; apply cases_on s' _ _; intros; intros r this,
id └──────┘ ┴ └──────┘ └┘
src ───────┘└────┘└──────┘┴ └──┘└┘└────┘└┘└────┘└──────┘┴ └──┘└┘└────┘└┘└───────────┘└─
typ ─────────────┘└──────┘┴┴└────┘└────┘└──────┘└──────┘┴└┘└────┘└────┘└┘└───────────┘└─
doc ───────┘└────┘ ┴ └──┘└┘└────┘└┘└────┘ ┴ └──┘└┘└────┘└┘└───────────┘└─
txt ───────┘└────┘ ┴ └──┘└┘└────┘└┘└────┘ ┴ └──┘└┘└────┘└┘└───────────┘└─
par ─────────────┘ ┴ └────┘└────┘└──────┘ ┴ └────┘└────┘└┘└───────────┘└─
pid ─────────────┘ ┴ └──────────────────┘ ┴ └────────────────────────────
st ─────────────────────────────────────────────────────────────────────────────────┘└─
260 { constructor, refl, assumption },
src ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
typ ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
doc ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
txt ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
par ─────────┘└─────────┘└┘└──┘└┘└─────────┘└──
pid ───────────────────────────────────────────
st ────────┘└──────────┘└────┘└───────────┘┴└─
261 { rw [destruct_nil, destruct_cons] at this,
id └──────────┘ └───────────┘
src ─────────┘└──┘└──────────┘└┘└───────────┘└───────┘└─
typ ─────────┘└──┘└──────────┘└┘└───────────┘└───────┘└─
doc ─────────┘└──┘ └┘ └───────┘└─
txt ─────────┘└──┘ └┘ └───────┘└─
par ─────────┘└──┘ └┘ └───────┘└─
pid ─────────────┘ └┘ └──────────
st ────────┘└───────────────┘└─────────────┘┴└──────┘└─
262 exact false.elim this },
id └────────┘ └──┘
src ───────────────┘└────────┘┴ └───
typ ───────────────┘└────────┘┴└──┘└───
doc ───────────────┘ ┴ └───
txt ───────────────┘ ┴ └───
par ───────────────┘ ┴ └───
pid ───────────────┘ ┴ └───
st ───────────────────────────────┘┴└─
263 { rw [destruct_nil, destruct_cons] at this,
id └──────────┘ └───────────┘
src ─────────┘└──┘└──────────┘└┘└───────────┘└───────┘└─
typ ─────────┘└──┘└──────────┘└┘└───────────┘└───────┘└─
doc ─────────┘└──┘ └┘ └───────┘└─
txt ─────────┘└──┘ └┘ └───────┘└─
par ─────────┘└──┘ └┘ └───────┘└─
pid ─────────────┘ └┘ └──────────
st ────────┘└───────────────┘└─────────────┘┴└──────┘└─
264 exact false.elim this },
id └────────┘ └──┘
src ───────────────┘└────────┘┴ └───
typ ───────────────┘└────────┘┴└──┘└───
doc ───────────────┘ ┴ └───
txt ───────────────┘ ┴ └───
par ───────────────┘ ┴ └───
pid ───────────────┘ ┴ └───
st ───────────────────────────────┘┴└─
265 { rw [destruct_cons, destruct_cons] at this,
id └───────────┘ └───────────┘
src ─────────┘└──┘└───────────┘└┘└───────────┘└───────┘└─
typ ─────────┘└──┘└───────────┘└┘└───────────┘└───────┘└─
doc ─────────┘└──┘ └┘ └───────┘└─
txt ─────────┘└──┘ └┘ └───────┘└─
par ─────────┘└──┘ └┘ └───────┘└─
pid ─────────────┘ └┘ └──────────
st ──────────────────────────┘└─────────────┘┴└──────┘└─
266 rw [head_cons, head_cons, tail_cons, tail_cons],
id └───────┘ └───────┘ └───────┘ └───────┘
src ─────────┘└──┘└───────┘└┘└───────┘└┘└───────┘└┘└───────┘┴└─
typ ─────────┘└──┘└───────┘└┘└───────┘└┘└───────┘└┘└───────┘┴└─
doc ─────────┘└──┘ └┘ └┘ └┘ ┴└─
txt ─────────┘└──┘ └┘ └┘ └┘ ┴└─
par ─────────┘└──┘ └┘ └┘ └┘ ┴└─
pid ─────────────┘ └┘ └┘ └┘ └──
st ──────────────────────┘└─────────┘└─────────┘└─────────┘└──
267 cases this with h1 h2,
id └──┘
src ─────────┘└────┘ └─────────┘└─
typ ─────────┘└────┘└──┘└─────────┘└─
doc ─────────┘└────┘ └─────────┘└─
txt ─────────┘└────┘ └─────────┘└─
par ─────────┘└────┘ └─────────┘└─
pid ───────────────┘ └────────────
st ──────────────────────────────┘└─
268 constructor, rw h1, exact h2 }
id └┘ └┘
src ─────────┘└─────────┘└┘└─┘ └──────┘ └──
typ ─────────┘└─────────┘└┘└─┘└┘└──────┘└┘└──
doc ─────────┘└─────────┘└┘└─┘ └──────┘ └──
txt ─────────┘└─────────┘└┘└─┘ └──────┘ └──
par ─────────┘└─────────┘└┘└─┘ └──────┘ └──
pid ─────────────────────────┘ └──────┘ └──
st ────────────────────┘└─────┘└─────────┘└─
269 end
src ──────────
typ ──────────
doc ──────────
txt ──────────
par ──────────
pid ──────────
st ────────┘└
270 end,
src ──────┘
typ ──────┘
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘└─
271 exact ⟨s₁, s₂, rfl, rfl, r⟩
id └┘ └┘ └─┘ ┴
src └────┘ └┘ └┘ └┘└─┘└┘ └─
typ └────┘ └┘└┘└┘└┘ └┘└─┘└┘┴└─
doc └────┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └─
pid ┴ └┘ └┘ └┘ └┘ ┴└
st ────────────────────────────────
272 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
273 end bisim
274
275 theorem coinduction : ∀ {s₁ s₂ : seq α}, head s₁ = head s₂ →
id ┴ └─┘ ┴ └──┘ └┘ ┴ └──┘ └┘
src └─┘ └──┘ ┴ └──┘
typ ┴ └─┘ ┴ └──┘ └┘ ┴ └──┘ └┘
doc └─┘ └──┘ └──┘
276 (∀ (β : Type u) (fr : seq α → β),
id ┴ └──┘ └─┘ ┴ ┴ ┴
src └─┘
typ ┴ └──┘ └─┘ ┴ ┴ ┴
doc └─┘
277 fr s₁ = fr s₂ → fr (tail s₁) = fr (tail s₂)) → s₁ = s₂
id └┘ └┘ ┴ └┘ └┘ └┘ └──┘ └┘ ┴ └┘ └──┘ └┘ └┘ ┴ └┘
src ┴ └──┘ ┴ └──┘ ┴
typ └┘ └┘ ┴ └┘ └┘ └┘ └──┘ └┘ ┴ └┘ └──┘ └┘ └┘ ┴ └┘
doc └──┘ └──┘
278 | ⟨f₁, a₁⟩ ⟨f₂, a₂⟩ hh ht :=
id └┘ └┘
typ └┘ └┘
279 subtype.eq (stream.coinduction hh (λ β fr, ht β (λs, fr s.1)))
id └────────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴┴
src └────────┘ └────────────────┘ ┴
typ └────────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴┴
280
281 theorem coinduction2 (s) (f g : seq α → seq β)
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
doc └─┘ └─┘
282 (H : ∀ s, bisim_o (λ (s1 s2 : seq β), ∃ (s : seq α), s1 = f s ∧ s2 = g s)
id ┴ └─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─────┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴
typ ┴ └─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └─┘ └─┘
283 (destruct (f s)) (destruct (g s)))
id └──────┘ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
284 : f s = g s :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
285 begin
st └─────
286 refine eq_of_bisim (λ s1 s2, ∃ s, s1 = f s ∧ s2 = g s) _ ⟨s, rfl, rfl⟩,
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └─────┘└─────────┘┴ └──────┘┴└┘┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘└─┘┴
typ └─────┘└─────────┘┴ └──────┘┴└┘┴┴ ┴┴┴┴┴ ┴ ┴ ┴ ┴┴┴ └──┘ ┴└┘ └┘└─┘┴
doc └─────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘ ┴
txt └─────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘ ┴
par └─────┘ ┴ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘ ┴
pid ┴ ┴ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
287 intros s1 s2 h, rcases h with ⟨s, h1, h2⟩,
id ┴
src └────────────┘ └─────┘ └───────────────┘
typ └────────────┘ └─────┘┴└───────────────┘
doc └────────────┘ └─────┘ └───────────────┘
txt └────────────┘ └─────┘ └───────────────┘
par └────────────┘ └─────┘ └───────────────┘
pid └──────┘ ┴ └───────────────┘
st ───────────────┘└─────────────────────────┘└─
288 rw [h1, h2], apply H
id └┘ └┘
src └──┘ └┘ ┴ └────┘ ┴
typ └──┘└┘└┘└┘┴ └────┘ ┴
doc └──┘ └┘ ┴ └────┘ ┴
txt └──┘ └┘ ┴ └────┘ ┴
par └──┘ └┘ ┴ └────┘ ┴
pid └┘ └┘ ┴ ┴ ┴
st ───────┘└──┘└─────────┘
289 end
st └─┘
290
291 /-- Embed an infinite stream as a sequence -/
292 def of_stream (s : stream α) : seq α :=
id └────┘ ┴ └─┘ ┴
src └────┘ └─┘
typ └────┘ ┴ └─┘ ┴
doc └─┘
293 ⟨s.map some, λn h, by contradiction⟩
id ┴└──┘ └──┘ ┴ ┴
src └──┘ └──┘ └───────────┘
typ ┴└──┘ └──┘ ┴ ┴ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
st └────────────┘
294
295 instance coe_stream : has_coe (stream α) (seq α) := ⟨of_stream⟩
id └─────┘ └────┘ ┴ └─┘ ┴ └───────┘
src └─────┘ └────┘ └─┘ └───────┘
typ └─────┘ └────┘ ┴ └─┘ ┴ └───────┘
doc └─┘ └───────┘
296
297 /-- Embed a `lazy_list α` as a sequence. Note that even though this
298 is non-meta, it will produce infinite sequences if used with
299 cyclic `lazy_list`s created by meta constructions. -/
300 def of_lazy_list : lazy_list α → seq α :=
id └───────┘ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ └─┘ ┴
doc └─┘
301 corec (λl, match l with
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
doc └───┘
302 | lazy_list.nil := none
id └───────────┘ └──┘
src └───────────┘ └──┘
typ └───────────┘ └──┘
303 | lazy_list.cons a l' := some (a, l' ())
id └────────────┘ ┴ └┘ └──┘ ┴ └┘
src └────────────┘ └──┘ ┴ └┘
typ └────────────┘ ┴ └┘ └──┘ ┴ └┘
304 end)
305
306 instance coe_lazy_list : has_coe (lazy_list α) (seq α) := ⟨of_lazy_list⟩
id └─────┘ └───────┘ ┴ └─┘ ┴ └──────────┘
src └─────┘ └───────┘ └─┘ └──────────┘
typ └─────┘ └───────┘ ┴ └─┘ ┴ └──────────┘
doc └─┘ └──────────┘
307
308 /-- Translate a sequence into a `lazy_list`. Since `lazy_list` and `list`
309 are isomorphic as non-meta types, this function is necessarily meta. -/
310 meta def to_lazy_list : seq α → lazy_list α | s :=
id └─┘ ┴ ┴ └───────┘ ┴ ┴
src └─┘ └───────┘
typ └─┘ ┴ ┴ └───────┘ ┴ ┴
doc └─┘
311 match destruct s with
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
312 | none := lazy_list.nil
id └──┘ └───────────┘
src └──┘ └───────────┘
typ └──┘ └───────────┘
313 | some (a, s') := lazy_list.cons a (to_lazy_list s')
id └──┘ ┴┴ └┘ └────────────┘ └──────────┘
src └──┘ ┴ └────────────┘
typ └──┘ ┴┴ └┘ └────────────┘ └──────────┘
314 end
315
316 /-- Translate a sequence to a list. This function will run forever if
317 run on an infinite sequence. -/
318 meta def force_to_list (s : seq α) : list α := (to_lazy_list s).to_list
id └─┘ ┴ └──┘ ┴ └──────────┘ ┴ └─────┘
src └─┘ └──┘ └──────────┘ └─────┘
typ └─┘ ┴ └──┘ ┴ └──────────┘ ┴ └─────┘
doc └─┘ └──────────┘
319
320 /-- The sequence of natural numbers some 0, some 1, ... -/
321 def nats : seq ℕ := stream.nats
id └─┘ ┴ └─────────┘
src └─┘ ┴ └─────────┘
typ └─┘ ┴ └─────────┘
doc └─┘
322
323 @[simp]
doc └──┘
324 lemma nats_nth (n : ℕ) : nats.nth n = some n := rfl
id ┴ └──┘└──┘ ┴ ┴ └──┘ ┴ └─┘
src ┴ └──┘└──┘ ┴ └──┘ └─┘
typ ┴ └──┘└──┘ ┴ ┴ └──┘ ┴ └─┘
doc └──┘└──┘
325
326 /-- Append two sequences. If `s₁` is infinite, then `s₁ ++ s₂ = s₁`,
327 otherwise it puts `s₂` at the location of the `nil` in `s₁`. -/
328 def append (s₁ s₂ : seq α) : seq α :=
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
doc └─┘ └─┘
329 @corec α (seq α × seq α) (λ⟨s₁, s₂⟩,
id └───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴└┘ └┘
src └───┘ └─┘ ┴ └─┘
typ └───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴└┘ └┘
doc └───┘ └─┘ └─┘
330 match destruct s₁ with
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
331 | none := omap (λs₂, (nil, s₂)) (destruct s₂)
id └──┘ └──┘ └┘ ┴└─┘ └┘ └──────┘
src └──┘ └──┘ ┴└─┘ └──────┘
typ └──┘ └──┘ └┘ ┴└─┘ └┘ └──────┘
doc └──┘ └─┘ └──────┘
332 | some (a, s₁') := some (a, s₁', s₂)
id └──┘ ┴┴ └─┘ └──┘ ┴
src └──┘ ┴ └──┘ ┴
typ └──┘ ┴┴ └─┘ └──┘ ┴
333 end) (s₁, s₂)
id ┴└┘ └┘
src ┴
typ ┴└┘ └┘
334
335 /-- Map a function over a sequence. -/
336 def map (f : α → β) : seq α → seq β | ⟨s, al⟩ :=
id ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
doc └─┘ └─┘
337 ⟨s.map (option.map f),
id └──┘ └────────┘ ┴
src └──┘ └────────┘
typ └──┘ └────────┘ ┴
338 λn, begin
id ┴
typ ┴
st └─────
339 dsimp [stream.map, stream.nth],
id └────────┘ └────────┘
src └─────┘└────────┘└┘└────────┘┴
typ └─────┘└────────┘└┘└────────┘┴
doc └─────┘ └┘ ┴
txt └─────┘ └┘ ┴
par └─────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ───────────────────────────────┘└─
340 induction e : s n; intro,
id ┴ ┴
src └────────┘ └─┘ ┴ └───┘
typ └────────┘ └─┘┴┴┴ └───┘
doc └────────┘ └─┘ ┴ └───┘
txt └────────┘ └─┘ ┴ └───┘
par └────────┘ └─┘ ┴ └───┘
pid ┴ └─┘ ┴
st ─────────────────────────┘└─
341 { rw al e, assumption }, { contradiction }
id └┘ ┴
src └─┘ ┴ └─────────┘ └────────────┘
typ └─┘└┘┴┴ └─────────┘ └────────────┘
doc └─┘ ┴ └─────────┘ └────────────┘
txt └─┘ ┴ └─────────┘ └────────────┘
par └─┘ ┴ └─────────┘ └────────────┘
pid ┴ ┴ ┴ ┴
st ───┘└─────┘└───────────┘└┘└───────────────┘└─
342 end⟩
st ──┘
343
344 /-- Flatten a sequence of sequences. (It is required that the
345 sequences be nonempty to ensure productivity; in the case
346 of an infinite sequence of `nil`, the first element is never
347 generated.) -/
348 def join : seq (seq1 α) → seq α :=
id └─┘ └──┘ ┴ └─┘ ┴
src └─┘ └──┘ └─┘
typ └─┘ └──┘ ┴ └─┘ ┴
doc └─┘ └──┘ └─┘
349 corec (λS, match destruct S with
id └───┘ ┴ └──────┘ ┴
src └───┘ └──────┘
typ └───┘ ┴ └──────┘ ┴
doc └───┘ └──────┘
350 | none := none
id └──┘ └──┘
src └──┘ └──┘
typ └──┘ └──┘
351 | some ((a, s), S') := some (a, match destruct s with
id └──┘ └┘┴ ┴ └┘ └──┘ ┴ └──────┘
src └──┘ └┘ └──┘ ┴ └──────┘
typ └──┘ └┘┴ ┴ └┘ └──┘ ┴ └──────┘
doc └──────┘
352 | none := S'
id └──┘
src └──┘
typ └──┘
353 | some s' := cons s' S'
id └──┘ └┘ └──┘
src └──┘ └──┘
typ └──┘ └┘ └──┘
doc └──┘
354 end)
355 end)
356
357 /-- Remove the first `n` elements from the sequence. -/
358 def drop (s : seq α) : ℕ → seq α
id └─┘ ┴ ┴ ┴ └─┘ ┴
src └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
359 | 0 := s
id ┴
typ ┴
360 | (n+1) := tail (drop n)
id ┴┴ └──┘ └──┘
src ┴ └──┘
typ ┴┴ └──┘ └──┘
doc └──┘
361 attribute [simp] drop
id └──┘
src └──┘
typ └──┘
doc └──┘ └──┘
362
363 /-- Take the first `n` elements of the sequence (producing a list) -/
364 def take : ℕ → seq α → list α
id ┴ ┴ └─┘ ┴ └──┘ ┴
src ┴ └─┘ └──┘
typ ┴ ┴ └─┘ ┴ └──┘ ┴
doc └─┘
365 | 0 s := []
id └┘
src └┘
typ └┘
366 | (n+1) s := match destruct s with
id ┴┴ ┴ └──────┘
src ┴ └──────┘
typ ┴┴ ┴ └──────┘
doc └──────┘
367 | none := []
id └──┘ └┘
src └──┘ └┘
typ └──┘ └┘
368 | some (x, r) := list.cons x (take n r)
id └──┘ ┴┴ ┴ └───────┘ └──┘
src └──┘ ┴ └───────┘
typ └──┘ ┴┴ ┴ └───────┘ └──┘
369 end
370
371 /-- Split a sequence at `n`, producing a finite initial segment
372 and an infinite tail. -/
373 def split_at : ℕ → seq α → list α × seq α
id ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴
src ┴ └─┘ └──┘ ┴ └─┘
typ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
374 | 0 s := ([], s)
id ┴ ┴└┘
src ┴└┘
typ ┴ ┴└┘
375 | (n+1) s := match destruct s with
id ┴┴ ┴ └──────┘
src ┴ └──────┘
typ ┴┴ ┴ └──────┘
doc └──────┘
376 | none := ([], nil)
id └──┘ ┴└┘ └─┘
src └──┘ ┴└┘ └─┘
typ └──┘ ┴└┘ └─┘
doc └─┘
377 | some (x, s') := let (l, r) := split_at n s' in (list.cons x l, r)
id └──┘ ┴┴ └┘ └─┘ ┴┴ ┴ └──────┘ ┴└───────┘
src └──┘ ┴ ┴ ┴└───────┘
typ └──┘ ┴┴ └┘ └─┘ ┴┴ ┴ └──────┘ ┴└───────┘
378 end
379
380 section zip_with
381
382 /-- Combine two sequences with a function -/
383 def zip_with (f : α → β → γ) : seq α → seq β → seq γ
id ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
384 | ⟨f₁, a₁⟩ ⟨f₂, a₂⟩ := ⟨λn,
id └┘ └┘ ┴
typ └┘ └┘ ┴
385 match f₁ n, f₂ n with
id ┴ ┴
typ ┴ ┴
386 | some a, some b := some (f a b)
id ┴ └──┘ ┴ └──┘ ┴
src └──┘ └──┘
typ ┴ └──┘ ┴ └──┘ ┴
387 | _, _ := none
id └──┘
src └──┘
typ └──┘
388 end,
389 λn, begin
id ┴
typ ┴
st └─────
390 induction h1 : f₁ n,
id └┘ ┴
src └────────┘ └─┘ ┴
typ └────────┘ └─┘└┘┴┴
doc └────────┘ └─┘ ┴
txt └────────┘ └─┘ ┴
par └────────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────────┘└─
391 { intro H, simp only [(a₁ h1)], refl },
id └┘ └┘
src └─────┘ └─────────┘ ┴ └┘ └───┘
typ └─────┘ └─────────┘ └┘┴└┘└┘ └───┘
doc └─────┘ └─────────┘ ┴ └┘ └───┘
txt └─────┘ └─────────┘ ┴ └┘ └───┘
par └─────┘ └─────────┘ ┴ └┘ └───┘
pid └┘ ┴└──┘└┘ ┴ └┘ ┴
st ─────┘└─────┘└───────────────────┘└─────┘└┘└
392 induction h2 : f₂ n; dsimp [seq.zip_with._match_1]; intro H,
id └┘ ┴ └───────────────────┘
src └────────┘ └─┘ ┴ └─────┘ ┴ └─────┘
typ └────────┘ └─┘└┘┴┴ └─────┘└───────────────────┘┴ └─────┘
doc └────────┘ └─┘ ┴ └─────┘ ┴ └─────┘
txt └────────┘ └─┘ ┴ └─────┘ ┴ └─────┘
par └────────┘ └─┘ ┴ └─────┘ ┴ └─────┘
pid ┴ └─┘ ┴ ┴┴ ┴ └┘
st ──────────────────────────────────────────────────────────────┘└─
393 { rw (a₂ h2), cases f₁ (n + 1); refl },
id └┘ └┘ └┘ ┴ ┴
src └─┘ ┴ ┴ └────┘ ┴ ┴┴└─┘ └───┘
typ └─┘ └┘┴└┘┴ └────┘└┘┴ ┴┴┴└─┘ └───┘
doc └─┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └───┘
txt └─┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └───┘
par └─┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └───┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
st ─────┘└────────┘└───────────────────────┘└┘└
394 { rw [h1, h2] at H, contradiction }
id └┘ └┘
src └──┘ └┘ └────┘ └────────────┘
typ └──┘└┘└┘└┘└────┘ └────────────┘
doc └──┘ └┘ └────┘ └────────────┘
txt └──┘ └┘ └────┘ └────────────┘
par └──┘ └┘ └────┘ └────────────┘
pid └┘ └┘ ┴└───┘ ┴
st ───────────┘└──┘┴└───┘└──────────────┘└─
395 end⟩
st ────┘
396
397 variables {s : seq α} {s' : seq β} {n : ℕ}
id └─┘ └─┘ ┴
src └─┘ └─┘ ┴
typ └─┘ └─┘ ┴
doc └─┘ └─┘
398
399 lemma zip_with_nth_some {a : α} {b : β} (s_nth_eq_some : s.nth n = some a)
id ┴ ┴ ┴└──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ ┴ ┴ ┴└──┘ ┴ ┴ └──┘ ┴
doc └──┘
400 (s_nth_eq_some' : s'.nth n = some b) (f : α → β → γ) :
id └┘└──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘ ┴ └──┘
typ └┘└──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
401 (zip_with f s s').nth n = some (f a b) :=
id └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──────┘ └─┘ ┴ └──┘
typ └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──────┘ └─┘
402 begin
st └─────
403 cases s with st,
id ┴
src └────┘ └──────┘
typ └────┘┴└──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └──────┘
st ────────────────┘└─
404 have : st n = some a, from s_nth_eq_some,
id └┘ ┴ ┴ └──┘ ┴ └───────────┘
src └─────┘ ┴ ┴┴┴└──┘┴ └───┘
typ └─────┘└┘┴┴┴┴┴└──┘┴┴ └───┘└───────────┘
doc └─────┘ ┴ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ └───┘
par └─────┘ ┴ ┴ ┴ ┴ └───┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └───┘
st ─────────────────────┘└──────────────────┘└─
405 cases s' with st',
id └┘
src └────┘ └───────┘
typ └────┘└┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ──────────────────┘└─
406 have : st' n = some b, from s_nth_eq_some',
id └─┘ ┴ └──┘ ┴ └────────────┘
src └─────┘ ┴ ┴ ┴└──┘┴ └───┘
typ └─────┘└─┘┴┴┴ ┴└──┘┴┴ └───┘└────────────┘
doc └─────┘ ┴ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ └───┘
par └─────┘ ┴ ┴ ┴ ┴ └───┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └───┘
st ──────────────────────┘└───────────────────┘└─
407 simp only [zip_with, seq.nth, *]
id └──────┘ └─────┘
src └─────────┘└──────┘└┘└─────┘└───┘
typ └─────────┘└──────┘└┘└─────┘└───┘
doc └─────────┘└──────┘└┘└─────┘└───┘
txt └─────────┘ └┘ └───┘
par └─────────┘ └┘ └───┘
pid ┴└──┘└┘ └┘ └──┘┴
st ──────────────────────────────────┘
408 end
st └─┘
409
410 lemma zip_with_nth_none (s_nth_eq_none : s.nth n = none) (f : α → β → γ) :
id ┴└──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ └──┘
typ ┴└──┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
411 (zip_with f s s').nth n = none :=
id └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └──┘
src └──────┘ └─┘ ┴ └──┘
typ └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └──┘
doc └──────┘ └─┘
412 begin
st └─────
413 cases s with st,
id ┴
src └────┘ └──────┘
typ └────┘┴└──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └──────┘
st ────────────────┘└─
414 have : st n = none, from s_nth_eq_none,
id └┘ ┴ ┴ └──┘ └───────────┘
src └─────┘ ┴ ┴┴┴└──┘ └───┘
typ └─────┘└┘┴┴┴┴┴└──┘ └───┘└───────────┘
doc └─────┘ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ └───┘
par └─────┘ ┴ ┴ ┴ └───┘
pid └───┘└┘ ┴ ┴ ┴ └───┘
st ───────────────────┘└──────────────────┘└─
415 cases s' with st',
id └┘
src └────┘ └───────┘
typ └────┘└┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ──────────────────┘└─
416 cases st'_nth_eq : st' n;
id └─┘ ┴
src └────┘ └─┘ ┴
typ └────┘ └─┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────────────────
417 simp only [zip_with, seq.nth, *]
id └──────┘ └─────┘
src └─────────┘└──────┘└┘└─────┘└───┘
typ └─────────┘└──────┘└┘└─────┘└───┘
doc └─────────┘└──────┘└┘└─────┘└───┘
txt └─────────┘ └┘ └───┘
par └─────────┘ └┘ └───┘
pid ┴└──┘└┘ └┘ └──┘┴
st ──────────────────────────────────┘
418 end
st └─┘
419
420 lemma zip_with_nth_none' (s'_nth_eq_none : s'.nth n = none) (f : α → β → γ) :
id └┘└──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ └──┘
typ └┘└──┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
421 (zip_with f s s').nth n = none :=
id └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └──┘
src └──────┘ └─┘ ┴ └──┘
typ └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └──┘
doc └──────┘ └─┘
422 begin
st └─────
423 cases s' with st',
id └┘
src └────┘ └───────┘
typ └────┘└┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ──────────────────┘└─
424 have : st' n = none, from s'_nth_eq_none,
id └─┘ ┴ ┴ └──┘ └────────────┘
src └─────┘ ┴ ┴┴┴└──┘ └───┘
typ └─────┘└─┘┴┴┴┴┴└──┘ └───┘└────────────┘
doc └─────┘ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ └───┘
par └─────┘ ┴ ┴ ┴ └───┘
pid └───┘└┘ ┴ ┴ ┴ └───┘
st ────────────────────┘└───────────────────┘└─
425 cases s with st,
id ┴
src └────┘ └──────┘
typ └────┘┴└──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └──────┘
st ────────────────┘└─
426 cases st_nth_eq : st n;
id └┘ ┴
src └────┘ └─┘ ┴
typ └────┘ └─┘└┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────────────
427 simp only [zip_with, seq.nth, *]
id └──────┘ └─────┘
src └─────────┘└──────┘└┘└─────┘└───┘
typ └─────────┘└──────┘└┘└─────┘└───┘
doc └─────────┘└──────┘└┘└─────┘└───┘
txt └─────────┘ └┘ └───┘
par └─────────┘ └┘ └───┘
pid ┴└──┘└┘ └┘ └──┘┴
st ──────────────────────────────────┘
428 end
st └─┘
429
430 end zip_with
431
432 /-- Pair two sequences into a sequence of pairs -/
433 def zip : seq α → seq β → seq (α × β) := zip_with prod.mk
id └─┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ └──────┘ └─────┘
src └─┘ └─┘ └─┘ ┴ └──────┘ └─────┘
typ └─┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ └──────┘ └─────┘
doc └─┘ └─┘ └─┘ └──────┘
434
435 /-- Separate a sequence of pairs into two sequences -/
436 def unzip (s : seq (α × β)) : seq α × seq β := (map prod.fst s, map prod.snd s)
id └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴└─┘ └──────┘ ┴ └─┘ └──────┘ ┴
src └─┘ ┴ └─┘ ┴ └─┘ ┴└─┘ └──────┘ └─┘ └──────┘
typ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴└─┘ └──────┘ ┴ └─┘ └──────┘ ┴
doc └─┘ └─┘ └─┘ └─┘ └─┘
437
438 /-- Convert a sequence which is known to terminate into a list -/
439 def to_list (s : seq α) (h : ∃ n, ¬ (nth s n).is_some) : list α :=
id └─┘ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─────┘ └──┘ ┴
src └─┘ ┴ ┴ ┴ └─┘ └─────┘ └──┘
typ └─┘ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─────┘ └──┘ ┴
doc └─┘ └─┘
440 take (nat.find h) s
id └──┘ └──────┘ ┴ ┴
src └──┘ └──────┘
typ └──┘ └──────┘ ┴ ┴
doc └──┘
441
442 /-- Convert a sequence which is known not to terminate into a stream -/
443 def to_stream (s : seq α) (h : ∀ n, (nth s n).is_some) : stream α :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ └────┘ ┴
src └─┘ └─┘ └─────┘ └────┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ └────┘ ┴
doc └─┘ └─┘
444 λn, option.get (h n)
id ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ └────────┘ ┴ ┴
445
446 /-- Convert a sequence into either a list or a stream depending on whether
447 it is finite or infinite. (Without decidability of the infiniteness predicate,
448 this is not constructively possible.) -/
449 def to_list_or_stream (s : seq α) [decidable (∃ n, ¬ (nth s n).is_some)] :
id └─┘ ┴ └───────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─────┘
src └─┘ └───────┘ ┴ ┴ ┴ └─┘ └─────┘
typ └─┘ ┴ └───────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─────┘
doc └─┘ └─┘
450 list α ⊕ stream α :=
id └──┘ ┴ ┴ └────┘ ┴
src └──┘ ┴ └────┘
typ └──┘ ┴ ┴ └────┘ ┴
451 if h : ∃ n, ¬ (nth s n).is_some
id └┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─────┘
src └┘ ┴ ┴ ┴ └─┘ └─────┘
typ └┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─────┘
doc └─┘
452 then sum.inl (to_list s h)
id └─────┘ └─────┘ ┴ ┴
src └─────┘ └─────┘
typ └─────┘ └─────┘ ┴ ┴
doc └─────┘
453 else sum.inr (to_stream s (λn, decidable.by_contradiction (λ hn, h ⟨n, hn⟩)))
id └─────┘ └───────┘ ┴ ┴ └────────────────────────┘ └┘ ┴ ┴ └┘
src └─────┘ └───────┘ └────────────────────────┘
typ └─────┘ └───────┘ ┴ ┴ └────────────────────────┘ └┘ ┴ ┴ └┘
doc └───────┘
454
455 @[simp] theorem nil_append (s : seq α) : append nil s = s :=
id └─┘ ┴ └────┘ └─┘ ┴ ┴ ┴
src └─┘ └────┘ └─┘ ┴
typ └─┘ ┴ └────┘ └─┘ ┴ ┴ ┴
doc └──┘ └─┘ └────┘ └─┘
456 begin
st └─────
457 apply coinduction2, intro s,
id └──────────┘
src └────┘└──────────┘ └─────┘
typ └────┘└──────────┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └┘
st ───────────────────┘└───────┘└─
458 dsimp [append], rw [corec_eq],
id └────┘ └──────┘
src └─────┘└────┘┴ └──┘└──────┘┴
typ └─────┘└────┘┴ └──┘└──────┘┴
doc └─────┘└────┘┴ └──┘ ┴
txt └─────┘ ┴ └──┘ ┴
par └─────┘ ┴ └──┘ ┴
pid ┴┴ ┴ └┘ ┴
st ───────────────┘└────────────┘└──
459 dsimp [append], apply cases_on s _ _,
id └────┘ └──────┘ ┴
src └─────┘└────┘┴ └────┘└──────┘┴ └──┘
typ └─────┘└────┘┴ └────┘└──────┘┴┴└──┘
doc └─────┘└────┘┴ └────┘ ┴ └──┘
txt └─────┘ ┴ └────┘ ┴ └──┘
par └─────┘ ┴ └────┘ ┴ └──┘
pid ┴┴ ┴ ┴ ┴ └──┘
st ───────────────┘└────────────────────┘└─
460 { trivial },
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ───┘└──────┘└┘└
461 { intros x s,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────────────┘└─
462 rw [destruct_cons], dsimp,
id └───────────┘
src └──┘└───────────┘┴ └───┘
typ └──┘└───────────┘┴ └───┘
doc └──┘ ┴ └───┘
txt └──┘ ┴ └───┘
par └──┘ ┴ └───┘
pid └┘ ┴
st ────────────────────┘└──────┘└─
463 exact ⟨rfl, s, rfl, rfl⟩ }
id ┴ └─┘
src └────┘ └┘ └┘ └┘└─┘└┘
typ └────┘ └┘┴└┘ └┘└─┘└┘
doc └────┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘
pid ┴ └┘ └┘ └┘ ┴┴
st ────────────────────────────┘└─
464 end
st ──┘
465
466 @[simp] theorem cons_append (a : α) (s t) : append (cons a s) t = cons a (append s t) :=
id ┴ └────┘ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴
src └────┘ └──┘ ┴ └──┘ └────┘
typ ┴ └────┘ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ ┴
doc └──┘ └────┘ └──┘ └──┘ └────┘
467 destruct_eq_cons $ begin
id └──────────────┘
src └──────────────┘
typ └──────────────┘
st └─────
468 dsimp [append], rw [corec_eq],
id └────┘ └──────┘
src └─────┘└────┘┴ └──┘└──────┘┴
typ └─────┘└────┘┴ └──┘└──────┘┴
doc └─────┘└────┘┴ └──┘ ┴
txt └─────┘ ┴ └──┘ ┴
par └─────┘ ┴ └──┘ ┴
pid ┴┴ ┴ └┘ ┴
st ───────────────┘└────────────┘└──
469 dsimp [append], rw [destruct_cons],
id └────┘ └───────────┘
src └─────┘└────┘┴ └──┘└───────────┘┴
typ └─────┘└────┘┴ └──┘└───────────┘┴
doc └─────┘└────┘┴ └──┘ ┴
txt └─────┘ ┴ └──┘ ┴
par └─────┘ ┴ └──┘ ┴
pid ┴┴ ┴ └┘ ┴
st ───────────────┘└─────────────────┘└──
470 dsimp [append], refl
id └────┘
src └─────┘└────┘┴ └───┘
typ └─────┘└────┘┴ └───┘
doc └─────┘└────┘┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴┴ ┴ ┴
st ───────────────┘└─────┘
471 end
st └─┘
472
473 @[simp] theorem append_nil (s : seq α) : append s nil = s :=
id └─┘ ┴ └────┘ ┴ └─┘ ┴ ┴
src └─┘ └────┘ └─┘ ┴
typ └─┘ ┴ └────┘ ┴ └─┘ ┴ ┴
doc └──┘ └─┘ └────┘ └─┘
474 begin
st └─────
475 apply coinduction2 s, intro s,
id └──────────┘ ┴
src └────┘└──────────┘┴ └─────┘
typ └────┘└──────────┘┴┴ └─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └┘
st ─────────────────────┘└───────┘└─
476 apply cases_on s _ _,
id └──────┘ ┴
src └────┘└──────┘┴ └──┘
typ └────┘└──────┘┴┴└──┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴ ┴ └──┘
st ─────────────────────┘└─
477 { trivial },
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ───┘└──────┘└┘└
478 { intros x s,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────────────┘└─
479 rw [cons_append, destruct_cons, destruct_cons], dsimp,
id └─────────┘ └───────────┘ └───────────┘
src └──┘└─────────┘└┘└───────────┘└┘└───────────┘┴ └───┘
typ └──┘└─────────┘└┘└───────────┘└┘└───────────┘┴ └───┘
doc └──┘ └┘ └┘ ┴ └───┘
txt └──┘ └┘ └┘ ┴ └───┘
par └──┘ └┘ └┘ ┴ └───┘
pid └┘ └┘ └┘ ┴
st ──────────────────┘└─────────────┘└─────────────┘└──────┘└─
480 exact ⟨rfl, s, rfl, rfl⟩ }
id ┴ └─┘
src └────┘ └┘ └┘ └┘└─┘└┘
typ └────┘ └┘┴└┘ └┘└─┘└┘
doc └────┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘
pid ┴ └┘ └┘ └┘ ┴┴
st ────────────────────────────┘└─
481 end
st ──┘
482
483 @[simp] theorem append_assoc (s t u : seq α) :
id └─┘ ┴
src └─┘
typ └─┘ ┴
doc └──┘ └─┘
484 append (append s t) u = append s (append t u) :=
id └────┘ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴
src └────┘ └────┘ ┴ └────┘ └────┘
typ └────┘ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴
doc └────┘ └────┘ └────┘ └────┘
485 begin
st └─────
486 apply eq_of_bisim (λs1 s2, ∃ s t u,
id └─────────┘ ┴ ┴
src └────┘└─────────┘┴ └─────┘┴└────┘┴└
typ └────┘└─────────┘┴ └─────┘┴└────┘┴└
doc └────┘ ┴ └─────┘ └────┘ └
txt └────┘ ┴ └─────┘ └────┘ └
par └────┘ ┴ └─────┘ └────┘ └
pid ┴ ┴ └─────┘ └────┘ └
st ──────────────────────────────────────
487 s1 = append (append s t) u ∧ s2 = append s (append t u)),
id ┴ ┴ └────┘
src ───┘ ┴┴┴ ┴ ┴ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘
typ ───┘ ┴┴┴ ┴ ┴ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘
doc ───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘
txt ───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par ───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────┘└─
488 { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, t, u, rfl, rfl⟩ := begin
id └┘ └┘ ┴ └─┘
src └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘└─┘└───┘ └
typ └────────────┘ └────┘ ┴└┘└┘└┘└┘┴└────┘ └┘ └┘ └┘ └┘ └┘ └┘└─┘└───┘ └
doc └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
txt └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
par └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
pid └──────┘ ┴ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
st ───┘└────────────┘└──────────────────────────────────────────────────────────┘└─────
489 apply cases_on s; simp,
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └┘└──┘└─
typ ───────────┘└──────┘┴┴└┘└──┘└─
doc ─────┘└────┘ ┴ └┘└──┘└─
txt ─────┘└────┘ ┴ └┘└──┘└─
par ───────────┘ ┴ └┘└──┘└─
pid ───────────┘ ┴ └───────
st ───────────────────────────┘└─
490 { apply cases_on t; simp,
id └──────┘ ┴
src ───────┘└────┘└──────┘┴ └┘└──┘└─
typ ─────────────┘└──────┘┴┴└┘└──┘└─
doc ───────┘└────┘ ┴ └┘└──┘└─
txt ───────┘└────┘ ┴ └┘└──┘└─
par ─────────────┘ ┴ └┘└──┘└─
pid ─────────────┘ ┴ └───────
st ──────┘└─────────────────────┘└─
491 { apply cases_on u; simp,
id └──────┘ ┴
src ─────────┘└────┘└──────┘┴ └┘└──┘└─
typ ───────────────┘└──────┘┴┴└┘└──┘└─
doc ─────────┘└────┘ ┴ └┘└──┘└─
txt ─────────┘└────┘ ┴ └┘└──┘└─
par ───────────────┘ ┴ └┘└──┘└─
pid ───────────────┘ ┴ └───────
st ────────┘└─────────────────────┘└─
492 { intros x u, refine ⟨nil, nil, u, _, _⟩; simp } },
id └─┘ ┴
src ───────────┘└────────┘└┘└─────┘ └┘└─┘└┘ └─────┘└┘└───┘└────
typ ───────────┘└────────┘└───────┘ └┘└─┘└┘┴└───────┘└───┘└────
doc ───────────┘└────────┘└┘└─────┘ └┘└─┘└┘ └─────┘└┘└───┘└────
txt ───────────┘└────────┘└┘└─────┘ └┘ └┘ └─────┘└┘└───┘└────
par ───────────┘└────────┘└───────┘ └┘ └┘ └───────┘└───┘└────
pid ──────────────────────────────┘ └┘ └┘ └──────────────────
st ─────────────────────┘└─────────────────────────────────┘└─┘└─
493 { intros x t, refine ⟨nil, t, u, _, _⟩; simp } },
id └─┘ ┴ ┴
src ─────────┘└────────┘└┘└─────┘ └─┘└┘ └┘ └─────┘└┘└───┘└────
typ ─────────┘└────────┘└───────┘ └─┘└┘┴└┘┴└───────┘└───┘└────
doc ─────────┘└────────┘└┘└─────┘ └─┘└┘ └┘ └─────┘└┘└───┘└────
txt ─────────┘└────────┘└┘└─────┘ └┘ └┘ └─────┘└┘└───┘└────
par ─────────┘└────────┘└───────┘ └┘ └┘ └───────┘└───┘└────
pid ────────────────────────────┘ └┘ └┘ └──────────────────
st ───────────────────┘└───────────────────────────────┘└─┘└─
494 { intros x s, exact ⟨s, t, u, rfl, rfl⟩ }
id ┴ ┴ ┴ └─┘
src ───────┘└────────┘└──────┘ └┘ └┘ └┘ └┘└─┘└───
typ ───────┘└────────┘└──────┘ ┴└┘┴└┘┴└┘ └┘└─┘└───
doc ───────┘└────────┘└──────┘ └┘ └┘ └┘ └┘ └───
txt ───────┘└────────┘└──────┘ └┘ └┘ └┘ └┘ └───
par ───────┘└────────┘└──────┘ └┘ └┘ └┘ └┘ └───
pid ─────────────────────────┘ └┘ └┘ └┘ └┘ └───
st ─────────────────┘└──────────────────────────┘└─
495 end end },
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ──────────┘┴
st ──────┘└───┘└┘└
496 { exact ⟨s, t, u, rfl, rfl⟩ }
id ┴ ┴ ┴ └─┘
src └────┘ └┘ └┘ └┘ └┘└─┘└┘
typ └────┘ ┴└┘┴└┘┴└┘ └┘└─┘└┘
doc └────┘ └┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘ └┘
pid ┴ └┘ └┘ └┘ └┘ ┴┴
st ─────────────────────────────┘└─
497 end
st ──┘
498
499 @[simp] theorem map_nil (f : α → β) : map f nil = nil := rfl
id ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └─┘
src └─┘ └─┘ ┴ └─┘ └─┘
typ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └─┘
doc └──┘ └─┘ └─┘ └─┘
500
501 @[simp] theorem map_cons (f : α → β) (a) : ∀ s, map f (cons a s) = cons (f a) (map f s)
id ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └──┘ ┴ └──┘ └─┘
typ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴
doc └──┘ └─┘ └──┘ └──┘ └─┘
502 | ⟨s, al⟩ := by apply subtype.eq; dsimp [cons, map]; rw stream.map_cons; refl
id └────────┘ └──┘ └─┘ └─────────────┘
src └────┘└────────┘ └─────┘└──┘└┘└─┘┴ └─┘└─────────────┘ └────
typ └────┘└────────┘ └─────┘└──┘└┘└─┘┴ └─┘└─────────────┘ └────
doc └────┘ └─────┘└──┘└┘└─┘┴ └─┘ └────
txt └────┘ └─────┘ └┘ ┴ └─┘ └────
par └────┘ └─────┘ └┘ ┴ └─┘ └────
pid ┴ ┴┴ └┘ ┴ ┴ └
st └───────────────────────────────────────┘└─────────────┘└──────
503
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
504 @[simp] theorem map_id : ∀ (s : seq α), map id s = s
id ┴ └─┘ ┴ └─┘ └┘ ┴ ┴ ┴
src └─┘ └─┘ └┘ ┴
typ ┴ └─┘ ┴ └─┘ └┘ ┴ ┴ ┴
doc └──┘ └─┘ └─┘
505 | ⟨s, al⟩ := begin
st └─────
506 apply subtype.eq; dsimp [map],
id └────────┘ └─┘
src └────┘└────────┘ └─────┘└─┘┴
typ └────┘└────────┘ └─────┘└─┘┴
doc └────┘ └─────┘└─┘┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ ┴┴ ┴
st ──────────────────────────────┘└─
507 rw [option.map_id, stream.map_id]; refl
id └───────────┘ └───────────┘
src └──┘└───────────┘└┘└───────────┘┴ └───┘
typ └──┘└───────────┘└┘└───────────┘┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st ──────────────────┘└─────────────┘┴└─────┘
508 end
st └─┘
509
510 @[simp] theorem map_tail (f : α → β) : ∀ s, map f (tail s) = tail (map f s)
id ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └──┘ └─┘ ┴ ┴
src └─┘ └──┘ ┴ └──┘ └─┘
typ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └──┘ └─┘ ┴ ┴
doc └──┘ └─┘ └──┘ └──┘ └─┘
511 | ⟨s, al⟩ := by apply subtype.eq; dsimp [tail, map]; rw stream.map_tail; refl
id └────────┘ └──┘ └─┘ └─────────────┘
src └────┘└────────┘ └─────┘└──┘└┘└─┘┴ └─┘└─────────────┘ └────
typ └────┘└────────┘ └─────┘└──┘└┘└─┘┴ └─┘└─────────────┘ └────
doc └────┘ └─────┘└──┘└┘└─┘┴ └─┘ └────
txt └────┘ └─────┘ └┘ ┴ └─┘ └────
par └────┘ └─────┘ └┘ ┴ └─┘ └────
pid ┴ ┴┴ └┘ ┴ ┴ └
st └───────────────────────────────────────┘└─────────────┘└──────
512
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
513 theorem map_comp (f : α → β) (g : β → γ) : ∀ (s : seq α), map (g ∘ f) s = map g (map f s)
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
src └─┘ └─┘ ┴ ┴ └─┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
doc └─┘ └─┘ └─┘ └─┘
514 | ⟨s, al⟩ := begin
st └─────
515 apply subtype.eq; dsimp [map],
id └────────┘ └─┘
src └────┘└────────┘ └─────┘└─┘┴
typ └────┘└────────┘ └─────┘└─┘┴
doc └────┘ └─────┘└─┘┴
txt └────┘ └─────┘ ┴
par └────┘ └─────┘ ┴
pid ┴ ┴┴ ┴
st ──────────────────────────────┘└─
516 rw stream.map_map,
id └────────────┘
src └─┘└────────────┘
typ └─┘└────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
517 apply congr_arg (λ f : _ → option γ, stream.map f s),
id └───────┘ ┴ └────┘ ┴ └────────┘ ┴
src └────┘└───────┘┴ └─────┘ ┴└────┘┴ └┘└────────┘┴ ┴ ┴
typ └────┘└───────┘┴ └─────┘┴┴└────┘┴┴└┘└────────┘┴ ┴┴┴
doc └────┘ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
txt └────┘ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
par └────┘ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────┘└─
518 funext x, cases x with x; refl
id ┴
src └──────┘ └────┘ └─────┘ └───┘
typ └──────┘ └────┘┴└─────┘ └───┘
doc └──────┘ └────┘ └─────┘ └───┘
txt └──────┘ └────┘ └─────┘ └───┘
par └──────┘ └────┘ └─────┘ └───┘
pid └┘ ┴ └─────┘ ┴
st ─────────┘└─────────────────────┘
519 end
st └─┘
520
521 @[simp] theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) (map f t) :=
id ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └────┘ ┴ └────┘ └─┘ └─┘
typ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └─┘ ┴ ┴
doc └──┘ └─┘ └────┘ └────┘ └─┘ └─┘
522 begin
st └─────
523 apply eq_of_bisim (λs1 s2, ∃ s t,
id └─────────┘ ┴ ┴
src └────┘└─────────┘┴ └─────┘┴└──┘┴└
typ └────┘└─────────┘┴ └─────┘┴└──┘┴└
doc └────┘ ┴ └─────┘ └──┘ └
txt └────┘ ┴ └─────┘ └──┘ └
par └────┘ ┴ └─────┘ └──┘ └
pid ┴ ┴ └─────┘ └──┘ └
st ────────────────────────────────────
524 s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _ ⟨s, t, rfl, rfl⟩,
id ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └─┘
src ───┘ ┴┴┴ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└────┘┴ ┴ ┴ └┘ └─┘┴ ┴ └───┘ └┘ └┘ └┘└─┘┴
typ ───┘ ┴┴┴ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└────┘┴ ┴ ┴ └┘ └─┘┴┴┴ └───┘ ┴└┘┴└┘ └┘└─┘┴
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└────┘┴ ┴ ┴ └┘ └─┘┴ ┴ └───┘ └┘ └┘ └┘ ┴
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ └┘ └┘ └┘ ┴
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ └┘ └┘ └┘ ┴
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────────────┘└─
525 intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, t, rfl, rfl⟩ := begin
id └┘ └┘ ┴
src └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
typ └────────────┘ └────┘ ┴└┘└┘└┘└┘┴└────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
doc └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
txt └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
par └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
pid └──────┘ ┴ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
st ───────────────┘└───────────────────────────────────────────────────────┘└─────
526 apply cases_on s; simp,
id └──────┘ ┴
src ───┘└────┘└──────┘┴ └┘└──┘└─
typ ─────────┘└──────┘┴┴└┘└──┘└─
doc ───┘└────┘ ┴ └┘└──┘└─
txt ───┘└────┘ ┴ └┘└──┘└─
par ─────────┘ ┴ └┘└──┘└─
pid ─────────┘ ┴ └───────
st ─────────────────────────┘└─
527 { apply cases_on t; simp,
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └┘└──┘└─
typ ───────────┘└──────┘┴┴└┘└──┘└─
doc ─────┘└────┘ ┴ └┘└──┘└─
txt ─────┘└────┘ ┴ └┘└──┘└─
par ───────────┘ ┴ └┘└──┘└─
pid ───────────┘ ┴ └───────
st ────┘└─────────────────────┘└─
528 { intros x t, refine ⟨nil, t, _, _⟩; simp } },
id └─┘ ┴
src ───────┘└────────┘└┘└─────┘ └─┘└┘ └─────┘└┘└───┘└────
typ ───────┘└────────┘└───────┘ └─┘└┘┴└───────┘└───┘└────
doc ───────┘└────────┘└┘└─────┘ └─┘└┘ └─────┘└┘└───┘└────
txt ───────┘└────────┘└┘└─────┘ └┘ └─────┘└┘└───┘└────
par ───────┘└────────┘└───────┘ └┘ └───────┘└───┘└────
pid ──────────────────────────┘ └┘ └──────────────────
st ─────────────────┘└────────────────────────────┘└─┘└─
529 { intros x s, refine ⟨s, t, rfl, rfl⟩ }
id ┴ ┴ └─┘
src ─────┘└────────┘└┘└─────┘ └┘ └┘ └┘└─┘└┘└─
typ ─────┘└────────┘└───────┘ ┴└┘┴└┘ └┘└─┘└───
doc ─────┘└────────┘└┘└─────┘ └┘ └┘ └┘ └┘└─
txt ─────┘└────────┘└┘└─────┘ └┘ └┘ └┘ └┘└─
par ─────┘└────────┘└───────┘ └┘ └┘ └┘ └───
pid ────────────────────────┘ └┘ └┘ └┘ └───
st ───────────────┘└────────────────────────┘└─
530 end end
src ─────────┘
typ ─────────┘
doc ─────────┘
txt ─────────┘
par ─────────┘
pid ────────┘┴
st ────┘└───┘
531 end
st └─┘
532
533 @[simp] theorem map_nth (f : α → β) : ∀ s n, nth (map f s) n = (nth s n).map f
id ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘ ┴ └─┘ └─┘
typ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └──┘ └─┘ └─┘ └─┘
534 | ⟨s, al⟩ n := rfl
id └─┘
src └─┘
typ └─┘
535
536 instance : functor seq := {map := @map}
id └─────┘ └─┘ └─┘
src └─────┘ └─┘ └─┘
typ └─────┘ └─┘ └─┘
doc └─┘ └─┘
537
538 instance : is_lawful_functor seq :=
id └───────────────┘ └─┘
src └───────────────┘ └─┘
typ └───────────────┘ └─┘
doc └─┘
539 { id_map := @map_id, comp_map := @map_comp }
id ┴ └────┘ └──────┘
src ┴ └────┘ └──────┘
typ ┴ └────┘ └──────┘
540
541 @[simp] theorem join_nil : join nil = (nil : seq α) := destruct_eq_nil rfl
id └──┘ └─┘ ┴ └─┘ └─┘ ┴ └─────────────┘ └─┘
src └──┘ └─┘ ┴ └─┘ └─┘ └─────────────┘ └─┘
typ └──┘ └─┘ ┴ └─┘ └─┘ ┴ └─────────────┘ └─┘
doc └──┘ └──┘ └─┘ └─┘ └─┘
542
543 @[simp] theorem join_cons_nil (a : α) (S) :
id ┴
typ ┴
doc └──┘
544 join (cons (a, nil) S) = cons a (join S) :=
id └──┘ └──┘ ┴┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ ┴
src └──┘ └──┘ ┴ └─┘ ┴ └──┘ └──┘
typ └──┘ └──┘ ┴┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ ┴
doc └──┘ └──┘ └─┘ └──┘ └──┘
545 destruct_eq_cons $ by simp [join]
id └──────────────┘ └──┘
src └──────────────┘ └────┘└──┘└─
typ └──────────────┘ └────┘└──┘└─
doc └────┘└──┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────
546
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
547 @[simp] theorem join_cons_cons (a b : α) (s S) :
id ┴
typ ┴
doc └──┘
548 join (cons (a, cons b s) S) = cons a (join (cons (b, s) S)) :=
id └──┘ └──┘ ┴┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ └──┘ ┴┴ ┴ ┴
src └──┘ └──┘ ┴ └──┘ ┴ └──┘ └──┘ └──┘ ┴
typ └──┘ └──┘ ┴┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ └──┘ ┴┴ ┴ ┴
doc └──┘ └──┘ └──┘ └──┘ └──┘ └──┘
549 destruct_eq_cons $ by simp [join]
id └──────────────┘ └──┘
src └──────────────┘ └────┘└──┘└─
typ └──────────────┘ └────┘└──┘└─
doc └────┘└──┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────
550
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
551 @[simp] theorem join_cons (a : α) (s S) :
id ┴
typ ┴
doc └──┘
552 join (cons (a, s) S) = cons a (append s (join S)) :=
id └──┘ └──┘ ┴┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ └──┘ ┴
src └──┘ └──┘ ┴ ┴ └──┘ └────┘ └──┘
typ └──┘ └──┘ ┴┴ ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘ └────┘ └──┘
553 begin
st └─────
554 apply eq_of_bisim (λs1 s2, s1 = s2 ∨
id └─────────┘ ┴ ┴
src └────┘└─────────┘┴ └─────┘ ┴┴┴ ┴┴└
typ └────┘└─────────┘┴ └─────┘ ┴┴┴ ┴┴└
doc └────┘ ┴ └─────┘ ┴ ┴ ┴ └
txt └────┘ ┴ └─────┘ ┴ ┴ ┴ └
par └────┘ ┴ └─────┘ ┴ ┴ ┴ └
pid ┴ ┴ └─────┘ ┴ ┴ ┴ └
st ───────────────────────────────────────
555 ∃ a s S, s1 = join (cons (a, s) S) ∧
id ┴ ┴ ┴ ┴
src ───┘┴└────┘┴┴ ┴ ┴ ┴ ┴┴ └┘ └┘ └┘┴└
typ ───┘┴└────┘┴┴ ┴ ┴ ┴ ┴┴ └┘ └┘ └┘┴└
doc ───┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └
txt ───┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └
par ───┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └
pid ───┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └
st ─────────────────────────────────────────
556 s2 = cons a (append s (join S))) _ (or.inr ⟨a, s, S, rfl, rfl⟩),
id └──┘ └────┘ └──┘ └────┘ ┴ ┴ ┴ └─┘
src ─────┘ ┴ ┴└──┘┴ ┴ └────┘┴ ┴ └──┘┴ └────┘ └────┘┴ └┘ └┘ └┘ └┘└─┘└┘
typ ─────┘ ┴ ┴└──┘┴ ┴ └────┘┴ ┴ └──┘┴ └────┘ └────┘┴ ┴└┘┴└┘┴└┘ └┘└─┘└┘
doc ─────┘ ┴ ┴└──┘┴ ┴ └────┘┴ ┴ └──┘┴ └────┘ ┴ └┘ └┘ └┘ └┘ └┘
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └┘ └┘ └┘ └┘ └┘
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └┘ └┘ └┘ └┘ └┘
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └┘ └┘ └┘ └┘ └┘
st ────────────────────────────────────────────────────────────────────┘└─
557 intros s1 s2 h,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───────────────┘└─
558 exact match s1, s2, h with
id └┘ └┘ ┴
src └────┘ ┴ └┘ └┘ └─────
typ └────┘ ┴└┘└┘└┘└┘┴└─────
doc └────┘ ┴ └┘ └┘ └─────
txt └────┘ ┴ └┘ └┘ └─────
par └────┘ ┴ └┘ └┘ └─────
pid ┴ ┴ └┘ └┘ └─────
st ─────────────────────────────
559 | _, _, (or.inl $ eq.refl s) := begin
id └────┘ └─────┘
src ─────────┘ └────┘┴ ┴└─────┘┴ └───┘ └
typ ─────────┘ └────┘┴ ┴└─────┘┴ └───┘ └
doc ─────────┘ ┴ ┴ ┴ └───┘ └
txt ─────────┘ ┴ ┴ ┴ └───┘ └
par ─────────┘ ┴ ┴ ┴ └───┘ └
pid ─────────┘ ┴ ┴ ┴ └───┘ └
st ─────────────────────────────────┘└─────
560 apply cases_on s, { trivial },
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └──┘└──────┘└──
typ ───────────┘└──────┘┴┴└──┘└──────┘└──
doc ─────┘└────┘ ┴ └──┘└──────┘└──
txt ─────┘└────┘ ┴ └──┘└──────┘└──
par ───────────┘ ┴ └──┘└──────┘└──
pid ───────────┘ ┴ └──────────────
st ─────────────────────┘└─┘└───────┘┴└─
561 { intros x s, rw [destruct_cons], exact ⟨rfl, or.inl rfl⟩ }
id └───────────┘ └────┘ └─┘
src ───────┘└────────┘└┘└──┘└───────────┘┴└──────┘ └┘└────┘┴└─┘└───
typ ───────┘└────────┘└┘└──┘└───────────┘┴└──────┘ └┘└────┘┴└─┘└───
doc ───────┘└────────┘└┘└──┘ ┴└──────┘ └┘ ┴ └───
txt ───────┘└────────┘└┘└──┘ ┴└──────┘ └┘ ┴ └───
par ───────┘└────────┘└┘└──┘ ┴└──────┘ └┘ ┴ └───
pid ───────────────────────┘ └───────┘ └┘ ┴ └───
st ─────────────────┘└─────────────────┘└─────────────────────────┘└─
562 end
src ────────
typ ────────
doc ────────
txt ────────
par ────────
pid ────────
st ──────┘└
563 | ._, ._, (or.inr ⟨a, s, S, rfl, rfl⟩) := begin
src ───┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └────┘ └
typ ───┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └────┘ └
doc ───┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └────┘ └
txt ───┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └────┘ └
par ───┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └────┘ └
pid ───┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └────┘ └
st ───────────────────────────────────────────┘└─────
564 apply cases_on s,
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └─
typ ───────────┘└──────┘┴┴└─
doc ─────┘└────┘ ┴ └─
txt ─────┘└────┘ ┴ └─
par ───────────┘ ┴ └─
pid ───────────┘ ┴ └─
st ─────────────────────┘└─
565 { simp },
src ───────┘└───┘└──
typ ───────┘└───┘└──
doc ───────┘└───┘└──
txt ───────┘└───┘└──
par ───────┘└───┘└──
pid ────────────────
st ──────┘└────┘┴└─
566 { intros x s, simp, refine or.inr ⟨x, s, S, rfl, rfl⟩ }
id └────┘ ┴ ┴ ┴ └─┘
src ───────┘└────────┘└┘└──┘└┘└─────┘└────┘┴ └┘ └┘ └┘ └┘└─┘└┘└─
typ ───────┘└────────┘└┘└──┘└───────┘└────┘┴ ┴└┘┴└┘┴└┘ └┘└─┘└───
doc ───────┘└────────┘└┘└──┘└┘└─────┘ ┴ └┘ └┘ └┘ └┘ └┘└─
txt ───────┘└────────┘└┘└──┘└┘└─────┘ ┴ └┘ └┘ └┘ └┘ └┘└─
par ───────┘└────────┘└┘└──┘└───────┘ ┴ └┘ └┘ └┘ └┘ └───
pid ────────────────────────────────┘ ┴ └┘ └┘ └┘ └┘ └───
st ─────────────────┘└────┘└──────────────────────────────────┘└─
567 end
src ────────
typ ────────
doc ────────
txt ────────
par ────────
pid ────────
st ──────┘└
568 end
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ────┘┴
st ─────┘
569 end
st └─┘
570
571 @[simp] theorem join_append (S T : seq (seq1 α)) :
id └─┘ └──┘ ┴
src └─┘ └──┘
typ └─┘ └──┘ ┴
doc └──┘ └─┘ └──┘
572 join (append S T) = append (join S) (join T) :=
id └──┘ └────┘ ┴ ┴ ┴ └────┘ └──┘ ┴ └──┘ ┴
src └──┘ └────┘ ┴ └────┘ └──┘ └──┘
typ └──┘ └────┘ ┴ ┴ ┴ └────┘ └──┘ ┴ └──┘ ┴
doc └──┘ └────┘ └────┘ └──┘ └──┘
573 begin
st └─────
574 apply eq_of_bisim (λs1 s2, ∃ s S T,
id └─────────┘ ┴ ┴
src └────┘└─────────┘┴ └─────┘┴└────┘┴└
typ └────┘└─────────┘┴ └─────┘┴└────┘┴└
doc └────┘ ┴ └─────┘ └────┘ └
txt └────┘ ┴ └─────┘ └────┘ └
par └────┘ ┴ └─────┘ └────┘ └
pid ┴ ┴ └─────┘ └────┘ └
st ──────────────────────────────────────
575 s1 = append s (join (append S T)) ∧
id ┴ ┴
src ───┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └─┘┴└
typ ───┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └─┘┴└
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ────────────────────────────────────────
576 s2 = append s (append (join S) (join T))),
id └────┘ └──┘
src ───┘ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘ └──┘┴ └─┘
typ ───┘ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘ └──┘┴ └─┘
doc ───┘ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘ └──┘┴ └─┘
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
st ────────────────────────────────────────────┘└─
577 { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, S, T, rfl, rfl⟩ := begin
id └┘ └┘ ┴ └─┘
src └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘└─┘└───┘ └
typ └────────────┘ └────┘ ┴└┘└┘└┘└┘┴└────┘ └┘ └┘ └┘ └┘ └┘ └┘└─┘└───┘ └
doc └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
txt └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
par └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
pid └──────┘ ┴ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
st ───┘└────────────┘└──────────────────────────────────────────────────────────┘└─────
578 apply cases_on s; simp,
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └┘└──┘└─
typ ───────────┘└──────┘┴┴└┘└──┘└─
doc ─────┘└────┘ ┴ └┘└──┘└─
txt ─────┘└────┘ ┴ └┘└──┘└─
par ───────────┘ ┴ └┘└──┘└─
pid ───────────┘ ┴ └───────
st ───────────────────────────┘└─
579 { apply cases_on S; simp,
id └──────┘ ┴
src ───────┘└────┘└──────┘┴ └┘└──┘└─
typ ─────────────┘└──────┘┴┴└┘└──┘└─
doc ───────┘└────┘ ┴ └┘└──┘└─
txt ───────┘└────┘ ┴ └┘└──┘└─
par ─────────────┘ ┴ └┘└──┘└─
pid ─────────────┘ ┴ └───────
st ──────┘└─────────────────────┘└─
580 { apply cases_on T, { simp },
id └──────┘ ┴
src ─────────┘└────┘└──────┘┴ └──┘└───┘└──
typ ───────────────┘└──────┘┴┴└──┘└───┘└──
doc ─────────┘└────┘ ┴ └──┘└───┘└──
txt ─────────┘└────┘ ┴ └──┘└───┘└──
par ───────────────┘ ┴ └──┘└───┘└──
pid ───────────────┘ ┴ └───────────
st ────────┘└───────────────┘└─┘└────┘┴└─
581 { intros s T, cases s with a s; simp,
id ┴
src ───────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
typ ───────────┘└────────┘└┘└────┘┴└───────┘└┘└──┘└─
doc ───────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
txt ───────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
par ───────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
pid ─────────────────────────────┘ └────────────────
st ─────────────────────┘└──────────────────────┘└─
582 refine ⟨s, nil, T, _, _⟩; simp } },
id ┴ └─┘ ┴
src ───────────┘└─────┘ └┘└─┘└┘ └─────┘└┘└───┘└────
typ ──────────────────┘ ┴└┘└─┘└┘┴└───────┘└───┘└────
doc ───────────┘└─────┘ └┘└─┘└┘ └─────┘└┘└───┘└────
txt ───────────┘└─────┘ └┘ └┘ └─────┘└┘└───┘└────
par ──────────────────┘ └┘ └┘ └───────┘└───┘└────
pid ──────────────────┘ └┘ └┘ └──────────────────
st ──────────────────────────────────────────┘└─┘└─
583 { intros s S, cases s with a s; simp,
id ┴
src ─────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
typ ─────────┘└────────┘└┘└────┘┴└───────┘└┘└──┘└─
doc ─────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
txt ─────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
par ─────────┘└────────┘└┘└────┘ └───────┘└┘└──┘└─
pid ───────────────────────────┘ └────────────────
st ───────────────────┘└──────────────────────┘└─
584 exact ⟨s, S, T, rfl, rfl⟩ } },
id ┴ ┴ ┴ └─┘
src ───────────────┘ └┘ └┘ └┘ └┘└─┘└──────
typ ───────────────┘ ┴└┘┴└┘┴└┘ └┘└─┘└──────
doc ───────────────┘ └┘ └┘ └┘ └┘ └──────
txt ───────────────┘ └┘ └┘ └┘ └┘ └──────
par ───────────────┘ └┘ └┘ └┘ └┘ └──────
pid ───────────────┘ └┘ └┘ └┘ └┘ └──────
st ───────────────────────────────────┘└─┘└─
585 { intros x s, exact ⟨s, S, T, rfl, rfl⟩ }
id ┴ ┴ ┴ └─┘
src ───────┘└────────┘└──────┘ └┘ └┘ └┘ └┘└─┘└───
typ ───────┘└────────┘└──────┘ ┴└┘┴└┘┴└┘ └┘└─┘└───
doc ───────┘└────────┘└──────┘ └┘ └┘ └┘ └┘ └───
txt ───────┘└────────┘└──────┘ └┘ └┘ └┘ └┘ └───
par ───────┘└────────┘└──────┘ └┘ └┘ └┘ └┘ └───
pid ─────────────────────────┘ └┘ └┘ └┘ └┘ └───
st ─────────────────┘└──────────────────────────┘└─
586 end end },
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ──────────┘┴
st ──────┘└───┘└┘└
587 { refine ⟨nil, S, T, _, _⟩; simp }
id └─┘ ┴ ┴
src └─────┘ └─┘└┘ └┘ └─────┘ └───┘
typ └─────┘ └─┘└┘┴└┘┴└─────┘ └───┘
doc └─────┘ └─┘└┘ └┘ └─────┘ └───┘
txt └─────┘ └┘ └┘ └─────┘ └───┘
par └─────┘ └┘ └┘ └─────┘ └───┘
pid ┴ └┘ └┘ └─────┘ ┴
st ──────────────────────────────────┘└─
588 end
st ──┘
589
590 @[simp] theorem of_list_nil : of_list [] = (nil : seq α) := rfl
id └─────┘ └┘ ┴ └─┘ └─┘ ┴ └─┘
src └─────┘ └┘ ┴ └─┘ └─┘ └─┘
typ └─────┘ └┘ ┴ └─┘ └─┘ ┴ └─┘
doc └──┘ └─────┘ └─┘ └─┘
591
592 @[simp] theorem of_list_cons (a : α) (l) :
id ┴
typ ┴
doc └──┘
593 of_list (a :: l) = cons a (of_list l) :=
id └─────┘ ┴ └┘ ┴ ┴ └──┘ ┴ └─────┘ ┴
src └─────┘ └┘ ┴ └──┘ └─────┘
typ └─────┘ ┴ └┘ ┴ ┴ └──┘ ┴ └─────┘ ┴
doc └─────┘ └──┘ └─────┘
594 begin
st └─────
595 apply subtype.eq, simp [of_list, cons],
id └────────┘ └─────┘ └──┘
src └────┘└────────┘ └────┘└─────┘└┘└──┘┴
typ └────┘└────────┘ └────┘└─────┘└┘└──┘┴
doc └────┘ └────┘└─────┘└┘└──┘┴
txt └────┘ └────┘ └┘ ┴
par └────┘ └────┘ └┘ ┴
pid ┴ ┴┴ └┘ ┴
st ─────────────────┘└────────────────────┘└─
596 funext n, cases n; simp [list.nth, stream.cons]
id ┴ └──────┘ └─────────┘
src └──────┘ └────┘ └────┘└──────┘└┘└─────────┘└┘
typ └──────┘ └────┘┴ └────┘└──────┘└┘└─────────┘└┘
doc └──────┘ └────┘ └────┘ └┘ └┘
txt └──────┘ └────┘ └────┘ └┘ └┘
par └──────┘ └────┘ └────┘ └┘ └┘
pid └┘ ┴ ┴┴ └┘ ┴┴
st ─────────┘└──────────────────────────────────────┘
597 end
st └─┘
598
599 @[simp] theorem of_stream_cons (a : α) (s) :
id ┴
typ ┴
doc └──┘
600 of_stream (a :: s) = cons a (of_stream s) :=
id └───────┘ ┴ └┘ ┴ ┴ └──┘ ┴ └───────┘ ┴
src └───────┘ └┘ ┴ └──┘ └───────┘
typ └───────┘ ┴ └┘ ┴ ┴ └──┘ ┴ └───────┘ ┴
doc └───────┘ └──┘ └───────┘
601 by apply subtype.eq; simp [of_stream, cons]; rw stream.map_cons
id └────────┘ └───────┘ └──┘ └─────────────┘
src └────┘└────────┘ └────┘└───────┘└┘└──┘┴ └─┘└─────────────┘└
typ └────┘└────────┘ └────┘└───────┘└┘└──┘┴ └─┘└─────────────┘└
doc └────┘ └────┘└───────┘└┘└──┘┴ └─┘ └
txt └────┘ └────┘ └┘ ┴ └─┘ └
par └────┘ └────┘ └┘ ┴ └─┘ └
pid ┴ ┴┴ └┘ ┴ ┴ └
st └────────────────────────────────────────────┘└─────────────┘└
602
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
603 @[simp] theorem of_list_append (l l' : list α) :
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
604 of_list (l ++ l') = append (of_list l) (of_list l') :=
id └─────┘ ┴ └┘ └┘ ┴ └────┘ └─────┘ ┴ └─────┘ └┘
src └─────┘ └┘ ┴ └────┘ └─────┘ └─────┘
typ └─────┘ ┴ └┘ └┘ ┴ └────┘ └─────┘ ┴ └─────┘ └┘
doc └─────┘ └────┘ └─────┘ └─────┘
605 by induction l; simp [*]
id ┴
src └────────┘ └────────
typ └────────┘┴ └────────
doc └────────┘ └────────
txt └────────┘ └────────
par └────────┘ └────────
pid ┴ ┴└─┘└
st └──────────────────────
606
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
607 @[simp] theorem of_stream_append (l : list α) (s : stream α) :
id └──┘ ┴ └────┘ ┴
src └──┘ └────┘
typ └──┘ ┴ └────┘ ┴
doc └──┘
608 of_stream (l ++ₛ s) = append (of_list l) (of_stream s) :=
id └───────┘ ┴ └─┘ ┴ ┴ └────┘ └─────┘ ┴ └───────┘ ┴
src └───────┘ └─┘ ┴ └────┘ └─────┘ └───────┘
typ └───────┘ ┴ └─┘ ┴ ┴ └────┘ └─────┘ ┴ └───────┘ ┴
doc └───────┘ └────┘ └─────┘ └───────┘
609 by induction l; simp [*, stream.nil_append_stream, stream.cons_append_stream]
id ┴ └──────────────────────┘ └───────────────────────┘
src └────────┘ └───────┘└──────────────────────┘└┘└───────────────────────┘└─
typ └────────┘┴ └───────┘└──────────────────────┘└┘└───────────────────────┘└─
doc └────────┘ └───────┘ └┘ └─
txt └────────┘ └───────┘ └┘ └─
par └────────┘ └───────┘ └┘ └─
pid ┴ ┴└──┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────
610
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
611 /-- Convert a sequence into a list, embedded in a computation to allow for
612 the possibility of infinite sequences (in which case the computation
613 never returns anything). -/
614 def to_list' {α} (s : seq α) : computation (list α) :=
id └─┘ ┴ └─────────┘ └──┘ ┴
src └─┘ └─────────┘ └──┘
typ └─┘ ┴ └─────────┘ └──┘ ┴
doc └─┘ └─────────┘
615 @computation.corec (list α) (list α × seq α) (λ⟨l, s⟩,
id └───────────────┘ └──┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴┴ ┴
src └───────────────┘ └──┘ └──┘ ┴ └─┘
typ └───────────────┘ └──┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴┴ ┴
doc └───────────────┘ └─┘
616 match destruct s with
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
617 | none := sum.inl l.reverse
id └──┘ └─────┘ └──────┘
src └──┘ └─────┘ └──────┘
typ └──┘ └─────┘ └──────┘
618 | some (a, s') := sum.inr (a::l, s')
id └──┘ ┴┴ └┘ └─────┘ ┴ └┘
src └──┘ ┴ └─────┘ ┴ └┘
typ └──┘ ┴┴ └┘ └─────┘ ┴ └┘
619 end) ([], s)
id ┴└┘ ┴
src ┴└┘
typ ┴└┘ ┴
620
621 theorem dropn_add (s : seq α) (m) : ∀ n, drop s (m + n) = drop (drop s m) n
id └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
src └─┘ └──┘ ┴ ┴ └──┘ └──┘
typ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴
doc └─┘ └──┘ └──┘ └──┘
622 | 0 := rfl
id └─┘
src └─┘
typ └─┘
623 | (n+1) := congr_arg tail (dropn_add n)
id ┴┴ └───────┘ └──┘ └───────┘
src ┴ └───────┘ └──┘
typ ┴┴ └───────┘ └──┘ └───────┘
doc └──┘
624
625 theorem dropn_tail (s : seq α) (n) : drop (tail s) n = drop s (n + 1) :=
id └─┘ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └─┘ └──┘ └──┘ ┴ └──┘ ┴
typ └─┘ ┴ └──┘ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └─┘ └──┘ └──┘ └──┘
626 by rw add_comm; symmetry; apply dropn_add
id └──────┘ └───────┘
src └─┘└──────┘ └──────┘ └────┘└───────┘└
typ └─┘└──────┘ └──────┘ └────┘└───────┘└
doc └─┘ └──────┘ └────┘ └
txt └─┘ └──────┘ └────┘ └
par └─┘ └──────┘ └────┘ └
pid ┴ ┴ └
st └───────────────────────────────────────
627
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
628 theorem nth_tail : ∀ (s : seq α) n, nth (tail s) n = nth s (n + 1)
id ┴ └─┘ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ └─┘ └──┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘ └──┘ └─┘
629 | ⟨f, al⟩ n := rfl
id └─┘
src └─┘
typ └─┘
630
631 @[ext]
doc └─┘
632 protected lemma ext (s s': seq α) (hyp : ∀ (n : ℕ), s.nth n = s'.nth n) : s = s' :=
id └─┘ ┴ ┴ ┴└──┘ ┴ ┴ └┘└──┘ ┴ ┴ ┴ └┘
src └─┘ ┴ └──┘ ┴ └──┘ ┴
typ └─┘ ┴ ┴ ┴└──┘ ┴ ┴ └┘└──┘ ┴ ┴ ┴ └┘
doc └─┘ └──┘ └──┘
633 begin
st └─────
634 let ext := (λ (s s' : seq α), ∀ n, s.nth n = s'.nth n),
id └─┘ ┴ └──┘ ┴ └──┘
src └─────────┘ └───────┘└─┘┴ └─┘ └┘ ┴ └──┘┴ ┴┴┴ └──┘┴ ┴
typ └─────────┘ └───────┘└─┘┴┴└─┘ └┘ ┴ └──┘┴ ┴┴┴ └──┘┴ ┴
doc └─────────┘ └───────┘└─┘┴ └─┘ └┘ ┴ └──┘┴ ┴ ┴ └──┘┴ ┴
txt └─────────┘ └───────┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────────┘ └───────┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘┴└─┘ └───────┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
635 apply seq.eq_of_bisim ext _ hyp,
id └─────────────┘ └─┘ └─┘
src └────┘└─────────────┘┴ └─┘
typ └────┘└─────────────┘┴└─┘└─┘└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ────────────────────────────────┘└─
636 -- we have to show that ext is a bisimulation
st ────────────────────────────────────────────────
637 clear hyp s s',
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └───────┘
st ───────────────┘└─
638 assume s s' (hyp : ext s s'),
id └─┘ ┴ └┘
src └─────────────────┘ ┴ ┴ ┴
typ └─────────────────┘└─┘┴┴┴└┘┴
doc └─────────────────┘ ┴ ┴ ┴
txt └─────────────────┘ ┴ ┴ ┴
par └─────────────────┘ ┴ ┴ ┴
pid └─────────────────┘ ┴ ┴ ┴
st ─────────────────────────────┘└─
639 unfold seq.destruct,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ────────────────────┘└─
640 rw (hyp 0),
id └─┘
src └─┘ └─┘
typ └─┘ └─┘└─┘
doc └─┘ └─┘
txt └─┘ └─┘
par └─┘ └─┘
pid ┴ └─┘
st ───────────┘└─
641 cases (s'.nth 0),
id └────┘
src └────┘ └────┘└─┘
typ └────┘ └────┘└─┘
doc └────┘ └────┘└─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────────────────┘└─
642 { simp [seq.bisim_o] }, -- option.none
id └─────────┘
src └────┘└─────────┘└┘
typ └────┘└─────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───┘└─────────────────┘└┘└───────────────
643 { -- option.some
st ───────────────────
644 suffices : ext s.tail s'.tail, by simpa,
id └─┘ └────┘ └─────┘
src └─────────┘ ┴└────┘┴└─────┘ └───┘
typ └─────────┘└─┘┴└────┘┴└─────┘ └───┘
doc └─────────┘ ┴└────┘┴└─────┘ └───┘
txt └─────────┘ ┴ ┴ └───┘
par └─────────┘ ┴ ┴ └───┘
pid └───────┘└┘ ┴ ┴
st ────────────────────────────────┘ └─
645 assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
646 simp only [seq.nth_tail _ n, (hyp $ n + 1)] }
id └──────────┘ ┴ └─┘ ┴ ┴
src └─────────┘└──────────┘└─┘ └┘ ┴ ┴ ┴┴└───┘
typ └─────────┘└──────────┘└─┘┴└┘ └─┘┴ ┴┴┴┴└───┘
doc └─────────┘ └─┘ └┘ ┴ ┴ ┴ └───┘
txt └─────────┘ └─┘ └┘ ┴ ┴ ┴ └───┘
par └─────────┘ └─┘ └┘ ┴ ┴ ┴ └───┘
pid ┴└──┘└┘ └─┘ └┘ ┴ ┴ ┴ └──┘┴
st ───────────────────────────────────────────────┘└─
647 end
st ──┘
648
649 @[simp] theorem head_dropn (s : seq α) (n) : head (drop s n) = nth s n :=
id └─┘ ┴ └──┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ └──┘ └──┘ ┴ └─┘
typ └─┘ ┴ └──┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └──┘ └─┘ └──┘ └──┘ └─┘
650 begin
st └─────
651 induction n with n IH generalizing s, { refl },
id ┴
src └────────┘ └───────────────────────┘ └───┘
typ └────────┘┴└───────────────────────┘ └───┘
doc └────────┘ └───────────────────────┘ └───┘
txt └────────┘ └───────────────────────┘ └───┘
par └────────┘ └───────────────────────┘ └───┘
pid ┴ ┴└───────┘└─────────────┘ ┴
st ─────────────────────────────────────┘└──┘└───┘└┘└
652 rw [nat.succ_eq_add_one, ←nth_tail, ←dropn_tail], apply IH
id └─────────────────┘ └──────┘ └────────┘
src └──┘└─────────────────┘└─┘└──────┘└─┘└────────┘┴ └────┘ ┴
typ └──┘└─────────────────┘└─┘└──────┘└─┘└────────┘┴ └────┘ ┴
doc └──┘ └─┘ └─┘ ┴ └────┘ ┴
txt └──┘ └─┘ └─┘ ┴ └────┘ ┴
par └──┘ └─┘ └─┘ ┴ └────┘ ┴
pid └┘ └─┘ └─┘ ┴ ┴ ┴
st ────────────────────────┘└─────────┘└───────────┘┴└─────────┘
653 end
st └─┘
654
655 theorem mem_map (f : α → β) {a : α} : ∀ {s : seq α}, a ∈ s → f a ∈ map f s
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─┘ └─┘
656 | ⟨g, al⟩ := stream.mem_map (option.map f)
id └────────────┘ └────────┘ ┴
src └────────────┘ └────────┘
typ └────────────┘ └────────┘ ┴
657
658 theorem exists_of_mem_map {f} {b : β} : ∀ {s : seq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b
id ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └─┘
659 | ⟨g, al⟩ h := let ⟨o, om, oe⟩ := stream.exists_of_mem_map h in
id ┴ └─┘ └──────────────────────┘
src └──────────────────────┘
typ ┴ └─┘ └──────────────────────┘
660 by cases o with a; injection oe with h'; exact ⟨a, om, h'⟩
id ┴ └┘ ┴ └┘ └┘
src └────┘ └─────┘ └────────┘ └──────┘ └────┘ └┘ └┘ └─
typ └────┘┴└─────┘ └────────┘└┘└──────┘ └────┘ ┴└┘└┘└┘└┘└─
doc └────┘ └─────┘ └────────┘ └──────┘ └────┘ └┘ └┘ └─
txt └────┘ └─────┘ └────────┘ └──────┘ └────┘ └┘ └┘ └─
par └────┘ └─────┘ └────────┘ └──────┘ └────┘ └┘ └┘ └─
pid ┴ └─────┘ ┴ └──────┘ ┴ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────
661
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
662 theorem of_mem_append {s₁ s₂ : seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂ :=
id └─┘ ┴ ┴ ┴ ┴ └────┘ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src └─┘ ┴ └────┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ └────┘ └┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘
doc └─┘ └────┘
663 begin
st └─────
664 have := h, revert this,
id ┴
src └──────┘ └─────────┘
typ └──────┘┴ └─────────┘
doc └──────┘ └─────────┘
txt └──────┘ └─────────┘
par └──────┘ └─────────┘
pid └───┘└─┘ └───┘
st ──────────┘└───────────┘└─
665 generalize e : append s₁ s₂ = ss, intro h, revert s₁,
id └────┘ └┘ └┘
src └─────────────┘└────┘┴ ┴ ┴ ┴ └─────┘ └───────┘
typ └─────────────┘└────┘┴└┘┴└┘┴ ┴ └─────┘ └───────┘
doc └─────────────┘└────┘┴ ┴ ┴ ┴ └─────┘ └───────┘
txt └─────────────┘ ┴ ┴ ┴ ┴ └─────┘ └───────┘
par └─────────────┘ ┴ ┴ ┴ ┴ └─────┘ └───────┘
pid └┘└┘┴ ┴ ┴ ┴ ┴ └┘ └─┘
st ─────────────────────────────────┘└───────┘└─────────┘└─
666 apply mem_rec_on h _,
id └────────┘ ┴
src └────┘└────────┘┴ └┘
typ └────┘└────────┘┴┴└┘
doc └────┘ ┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴ ┴ └┘
st ─────────────────────┘└─
667 intros b s' o s₁,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────┘└─
668 apply s₁.cases_on _ (λ c t₁, _); intros m e;
id └─────────┘
src └────┘└─────────┘└─┘ └───────┘ └────────┘
typ └────┘└─────────┘└─┘ └───────┘ └────────┘
doc └────┘ └─┘ └───────┘ └────────┘
txt └────┘ └─┘ └───────┘ └────────┘
par └────┘ └─┘ └───────┘ └────────┘
pid ┴ └─┘ └───────┘ └──┘
st ───────────────────────────────────────────────
669 have := congr_arg destruct e,
id └───────┘ └──────┘ ┴
src └──────┘└───────┘┴└──────┘┴
typ └──────┘└───────┘┴└──────┘┴┴
doc └──────┘ ┴└──────┘┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ─────────────────────────────┘└─
670 { apply or.inr, simpa using m },
id └────┘ ┴
src └────┘└────┘ └──────────┘ ┴
typ └────┘└────┘ └──────────┘┴┴
doc └────┘ └──────────┘ ┴
txt └────┘ └──────────┘ ┴
par └────┘ └──────────┘ ┴
pid ┴ ┴└────┘ ┴
st ───┘└──────────┘└──────────────┘└┘└
671 { cases (show a = c ∨ a ∈ append t₁ s₂, by simpa using m) with e' m,
id ┴ ┴ ┴ ┴ └────┘ └┘ └┘ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴┴┴└────┘┴ ┴ └───┘└──────────┘ └─────────┘
typ └────┘ ┴ ┴ ┴┴┴┴┴┴┴┴┴└────┘┴└┘┴└┘└───┘└──────────┘┴└─────────┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘┴ ┴ └───┘└──────────┘ └─────────┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└──────────┘ └─────────┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└──────────┘ └─────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴└────────┘
st ───────────────────────────────────────────┘└────────────┘└─────────┘└─
672 { rw e', exact or.inl (mem_cons _ _) },
id └┘ └────┘ └──────┘
src └─┘ └────┘└────┘┴ └──────┘└────┘
typ └─┘└┘ └────┘└────┘┴ └──────┘└────┘
doc └─┘ └────┘ ┴ └────┘
txt └─┘ └────┘ ┴ └────┘
par └─┘ └────┘ ┴ └────┘
pid ┴ ┴ ┴ └───┘┴
st ─────┘└───┘└────────────────────────────┘└┘└
673 { cases (show c = b ∧ append t₁ s₂ = s', by simpa) with i1 i2,
id ┴ ┴ ┴ └────┘ └┘ └┘ └┘
src └────┘ ┴ ┴ ┴ ┴ ┴└────┘┴ ┴ ┴ ┴ └───┘└───┘└──────────┘
typ └────┘ ┴┴┴ ┴┴┴┴┴└────┘┴└┘┴└┘┴ ┴└┘└───┘└───┘└──────────┘
doc └────┘ ┴ ┴ ┴ ┴ ┴└────┘┴ ┴ ┴ ┴ └───┘└───┘└──────────┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└───┘└──────────┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└───┘└──────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└─────────┘
st ──────────────────────────────────────────────┘└────┘└──────────┘└─
674 cases o with e' IH,
id ┴
src └────┘ └─────────┘
typ └────┘┴└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ───────────────────────┘└─
675 { simp [i1, e'] },
id └┘ └┘
src └────┘ └┘ └┘
typ └────┘└┘└┘└┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───────┘└────────────┘└┘└
676 { exact or.imp_left (mem_cons_of_mem _) (IH m i2) } } }
id └─────────┘ └─────────────┘ └┘ ┴ └┘
src └────┘└─────────┘┴ └─────────────┘└──┘ ┴ ┴ └┘
typ └────┘└─────────┘┴ └─────────────┘└──┘ └┘┴┴┴└┘└┘
doc └────┘ ┴ └──┘ ┴ ┴ └┘
txt └────┘ ┴ └──┘ ┴ ┴ └┘
par └────┘ ┴ └──┘ ┴ ┴ └┘
pid ┴ ┴ └──┘ ┴ ┴ ┴┴
st ───────────────────────────────────────────────────────┘└─────
677 end
st ──┘
678
679 theorem mem_append_left {s₁ s₂ : seq α} {a : α} (h : a ∈ s₁) : a ∈ append s₁ s₂ :=
id └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └────┘ └┘ └┘
src └─┘ ┴ ┴ └────┘
typ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └────┘ └┘ └┘
doc └─┘ └────┘
680 by apply mem_rec_on h; intros; simp [*]
id └────────┘ ┴
src └────┘└────────┘┴ └────┘ └────────
typ └────┘└────────┘┴┴ └────┘ └────────
doc └────┘ ┴ └────┘ └────────
txt └────┘ ┴ └────┘ └────────
par └────┘ ┴ └────┘ └────────
pid ┴ ┴ ┴└─┘└
st └─────────────────────────────────────
681
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
682 end seq
683
684 namespace seq1
685 variables {α : Type u} {β : Type v} {γ : Type w}
686 open seq
687
688 /-- Convert a `seq1` to a sequence. -/
689 def to_seq : seq1 α → seq α
id └──┘ ┴ ┴ └─┘ ┴
src └──┘ └─┘
typ └──┘ ┴ ┴ └─┘ ┴
doc └──┘ └─┘
690 | (a, s) := cons a s
id ┴┴ ┴ └──┘
src ┴ └──┘
typ ┴┴ ┴ └──┘
doc └──┘
691
692 instance coe_seq : has_coe (seq1 α) (seq α) := ⟨to_seq⟩
id └─────┘ └──┘ ┴ └─┘ ┴ └────┘
src └─────┘ └──┘ └─┘ └────┘
typ └─────┘ └──┘ ┴ └─┘ ┴ └────┘
doc └──┘ └─┘ └────┘
693
694 /-- Map a function on a `seq1` -/
695 def map (f : α → β) : seq1 α → seq1 β
id ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └──┘ └──┘
typ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
696 | (a, s) := (f a, seq.map f s)
id ┴┴ ┴ ┴┴ └─────┘ ┴
src ┴ ┴ └─────┘
typ ┴┴ ┴ ┴┴ └─────┘ ┴
doc └─────┘
697
698 theorem map_id : ∀ (s : seq1 α), map id s = s | ⟨a, s⟩ := by simp [map]
id ┴ └──┘ ┴ └─┘ └┘ ┴ ┴ ┴ └─┘
src └──┘ └─┘ └┘ ┴ └────┘└─┘└─
typ ┴ └──┘ ┴ └─┘ └┘ ┴ ┴ ┴ └────┘└─┘└─
doc └──┘ └─┘ └────┘└─┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
699
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
700 /-- Flatten a nonempty sequence of nonempty sequences -/
701 def join : seq1 (seq1 α) → seq1 α
id └──┘ └──┘ ┴ ┴ └──┘ ┴
src └──┘ └──┘ └──┘
typ └──┘ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘
702 | ((a, s), S) := match destruct s with
id └┘┴ ┴ ┴ └──────┘
src └┘ └──────┘
typ └┘┴ ┴ ┴ └──────┘
doc └──────┘
703 | none := (a, seq.join S)
id └──┘ ┴ └──────┘
src └──┘ ┴ └──────┘
typ └──┘ ┴ └──────┘
doc └──────┘
704 | some s' := (a, seq.join (cons s' S))
id └──┘ └┘ ┴ └──────┘ └──┘
src └──┘ ┴ └──────┘ └──┘
typ └──┘ └┘ ┴ └──────┘ └──┘
doc └──────┘ └──┘
705 end
706
707 @[simp] theorem join_nil (a : α) (S) : join ((a, nil), S) = (a, seq.join S) := rfl
id ┴ └──┘ └┘┴ └─┘ ┴ ┴ ┴┴ └──────┘ ┴ └─┘
src └──┘ └┘ └─┘ ┴ ┴ └──────┘ └─┘
typ ┴ └──┘ └┘┴ └─┘ ┴ ┴ ┴┴ └──────┘ ┴ └─┘
doc └──┘ └──┘ └─┘ └──────┘
708
709 @[simp] theorem join_cons (a b : α) (s S) :
id ┴
typ ┴
doc └──┘
710 join ((a, cons b s), S) = (a, seq.join (cons (b, s) S)) :=
id └──┘ └┘┴ └──┘ ┴ ┴ ┴ ┴ ┴┴ └──────┘ └──┘ ┴┴ ┴ ┴
src └──┘ └┘ └──┘ ┴ ┴ └──────┘ └──┘ ┴
typ └──┘ └┘┴ └──┘ ┴ ┴ ┴ ┴ ┴┴ └──────┘ └──┘ ┴┴ ┴ ┴
doc └──┘ └──┘ └──────┘ └──┘
711 by dsimp [join]; rw [destruct_cons]; refl
id └──┘ └───────────┘
src └─────┘└──┘┴ └──┘└───────────┘┴ └────
typ └─────┘└──┘┴ └──┘└───────────┘┴ └────
doc └─────┘└──┘┴ └──┘ ┴ └────
txt └─────┘ ┴ └──┘ ┴ └────
par └─────┘ ┴ └──┘ ┴ └────
pid ┴┴ ┴ └┘ ┴ └
st └─────────────────┘└───────────┘┴└──────
712
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
713 /-- The `return` operator for the `seq1` monad,
714 which produces a singleton sequence. -/
715 def ret (a : α) : seq1 α := (a, nil)
id ┴ └──┘ ┴ ┴┴ └─┘
src └──┘ ┴ └─┘
typ ┴ └──┘ ┴ ┴┴ └─┘
doc └──┘ └─┘
716
717 instance [inhabited α] : inhabited (seq1 α) := ⟨ret (default _)⟩
id └───────┘ ┴ └───────┘ └──┘ ┴ └─┘ └─────┘
src └───────┘ └───────┘ └──┘ └─┘ └─────┘
typ └───────┘ ┴ └───────┘ └──┘ ┴ └─┘ └─────┘
doc └──┘ └─┘
718
719 /-- The `bind` operator for the `seq1` monad,
720 which maps `f` on each element of `s` and appends the results together.
721 (Not all of `s` may be evaluated, because the first few elements of `s`
722 may already produce an infinite result.) -/
723 def bind (s : seq1 α) (f : α → seq1 β) : seq1 β :=
id └──┘ ┴ ┴ └──┘ ┴ └──┘ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ ┴ └──┘ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘
724 join (map f s)
id └──┘ └─┘ ┴ ┴
src └──┘ └─┘
typ └──┘ └─┘ ┴ ┴
doc └──┘ └─┘
725
726 @[simp] theorem join_map_ret (s : seq α) : seq.join (seq.map ret s) = s :=
id └─┘ ┴ └──────┘ └─────┘ └─┘ ┴ ┴ ┴
src └─┘ └──────┘ └─────┘ └─┘ ┴
typ └─┘ ┴ └──────┘ └─────┘ └─┘ ┴ ┴ ┴
doc └──┘ └─┘ └──────┘ └─────┘ └─┘
727 by apply coinduction2 s; intro s; apply cases_on s; simp [ret]
id └──────────┘ ┴ └──────┘ ┴ └─┘
src └────┘└──────────┘┴ └─────┘ └────┘└──────┘┴ └────┘└─┘└─
typ └────┘└──────────┘┴┴ └─────┘ └────┘└──────┘┴┴ └────┘└─┘└─
doc └────┘ ┴ └─────┘ └────┘ ┴ └────┘└─┘└─
txt └────┘ ┴ └─────┘ └────┘ ┴ └────┘ └─
par └────┘ ┴ └─────┘ └────┘ ┴ └────┘ └─
pid ┴ ┴ └┘ ┴ ┴ ┴┴ ┴└
st └────────────────────────────────────────────────────────────
728
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
729 @[simp] theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
id ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └──┘ └─┘ ┴ ┴ └─┘
typ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └──┘ └──┘ └─┘ └─┘
730 | ⟨a, s⟩ := begin
st └─────
731 dsimp [bind, map], change (λx, ret (f x)) with (ret ∘ f),
id └──┘ └─┘ └─┘ ┴ └─┘ ┴ ┴
src └─────┘└──┘└┘└─┘┴ └─────┘ └─┘└─┘┴ ┴ └──────┘ └─┘┴┴┴ ┴
typ └─────┘└──┘└┘└─┘┴ └─────┘ └─┘└─┘┴ ┴┴ └──────┘ └─┘┴┴┴┴┴
doc └─────┘└──┘└┘└─┘┴ └─────┘ └─┘└─┘┴ ┴ └──────┘ └─┘┴ ┴ ┴
txt └─────┘ └┘ ┴ └─────┘ └─┘ ┴ ┴ └──────┘ ┴ ┴ ┴
par └─────┘ └┘ ┴ └─────┘ └─┘ ┴ ┴ └──────┘ ┴ ┴ ┴
pid ┴┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘└────┘ ┴ ┴ ┴
st ──────────────────┘└────────────────────────────────────────
732 rw [map_comp], simp [function.comp, ret]
id └──────┘ └───────────┘ └─┘
src └──┘└──────┘┴ └────┘└───────────┘└┘└─┘└┘
typ └──┘└──────┘┴ └────┘└───────────┘└┘└─┘└┘
doc └──┘ ┴ └────┘ └┘└─┘└┘
txt └──┘ ┴ └────┘ └┘ └┘
par └──┘ ┴ └────┘ └┘ └┘
pid └┘ ┴ ┴┴ └┘ ┴┴
st ─────────────┘└───────────────────────────┘
733 end
st └─┘
734
735 @[simp] theorem ret_bind (a : α) (f : α → seq1 β) : bind (ret a) f = f a :=
id ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ └─┘ ┴
typ ┴ ┴ └──┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘ └──┘ └─┘
736 begin
st └─────
737 simp [ret, bind, map],
id └─┘ └──┘ └─┘
src └────┘└─┘└┘└──┘└┘└─┘┴
typ └────┘└─┘└┘└──┘└┘└─┘┴
doc └────┘└─┘└┘└──┘└┘└─┘┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ──────────────────────┘└─
738 cases f a with a s,
id ┴ ┴
src └────┘ ┴ └───────┘
typ └────┘┴┴┴└───────┘
doc └────┘ ┴ └───────┘
txt └────┘ ┴ └───────┘
par └────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ───────────────────┘└─
739 apply cases_on s; intros; simp
id └──────┘ ┴
src └────┘└──────┘┴ └────┘ └───┘
typ └────┘└──────┘┴┴ └────┘ └───┘
doc └────┘ ┴ └────┘ └───┘
txt └────┘ ┴ └────┘ └───┘
par └────┘ ┴ └────┘ └───┘
pid ┴ ┴ ┴
st ────────────────────────────────┘
740 end
st └─┘
741
742 @[simp] theorem map_join' (f : α → β) (S) :
id ┴ ┴
typ ┴ ┴
doc └──┘
743 seq.map f (seq.join S) = seq.join (seq.map (map f) S) :=
id └─────┘ ┴ └──────┘ ┴ ┴ └──────┘ └─────┘ └─┘ ┴ ┴
src └─────┘ └──────┘ ┴ └──────┘ └─────┘ └─┘
typ └─────┘ ┴ └──────┘ ┴ ┴ └──────┘ └─────┘ └─┘ ┴ ┴
doc └─────┘ └──────┘ └──────┘ └─────┘ └─┘
744 begin
st └─────
745 apply eq_of_bisim (λs1 s2,
id └─────────┘
src └────┘└─────────┘┴ └──────
typ └────┘└─────────┘┴ └──────
doc └────┘ ┴ └──────
txt └────┘ ┴ └──────
par └────┘ ┴ └──────
pid ┴ ┴ └──────
st ─────────────────────────────
746 ∃ s S, s1 = append s (seq.map f (seq.join S)) ∧
id ┴ ┴ ┴ ┴
src ───┘┴└──┘┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └─┘┴└
typ ───┘┴└──┘┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └─┘┴└
doc ───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
txt ───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ────────────────────────────────────────────────────
747 s2 = append s (seq.join (seq.map (map f) S))),
id └────┘ └──────┘ └─────┘ └─┘ ┴
src ─────┘ ┴ ┴└────┘┴ ┴ └──────┘┴ └─────┘┴ └─┘┴ └┘ └─┘
typ ─────┘ ┴ ┴└────┘┴ ┴ └──────┘┴ └─────┘┴ └─┘┴┴└┘ └─┘
doc ─────┘ ┴ ┴└────┘┴ ┴ └──────┘┴ └─────┘┴ └─┘┴ └┘ └─┘
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
st ──────────────────────────────────────────────────┘└─
748 { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, S, rfl, rfl⟩ := begin
id └┘ └┘ ┴ └─┘
src └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘└─┘└───┘ └
typ └────────────┘ └────┘ ┴└┘└┘└┘└┘┴└────┘ └┘ └┘ └┘ └┘ └┘└─┘└───┘ └
doc └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
txt └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
par └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
pid └──────┘ ┴ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
st ───┘└────────────┘└───────────────────────────────────────────────────────┘└─────
749 apply cases_on s; simp,
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └┘└──┘└─
typ ───────────┘└──────┘┴┴└┘└──┘└─
doc ─────┘└────┘ ┴ └┘└──┘└─
txt ─────┘└────┘ ┴ └┘└──┘└─
par ───────────┘ ┴ └┘└──┘└─
pid ───────────┘ ┴ └───────
st ───────────────────────────┘└─
750 { apply cases_on S; simp,
id └──────┘ ┴
src ───────┘└────┘└──────┘┴ └┘└──┘└─
typ ─────────────┘└──────┘┴┴└┘└──┘└─
doc ───────┘└────┘ ┴ └┘└──┘└─
txt ───────┘└────┘ ┴ └┘└──┘└─
par ─────────────┘ ┴ └┘└──┘└─
pid ─────────────┘ ┴ └───────
st ──────┘└─────────────────────┘└─
751 { intros x S, cases x with a s; simp [map],
id ┴ └─┘
src ─────────┘└────────┘└┘└────┘ └───────┘└┘└────┘└─┘┴└─
typ ─────────┘└────────┘└┘└────┘┴└───────┘└┘└────┘└─┘┴└─
doc ─────────┘└────────┘└┘└────┘ └───────┘└┘└────┘└─┘┴└─
txt ─────────┘└────────┘└┘└────┘ └───────┘└┘└────┘ ┴└─
par ─────────┘└────────┘└┘└────┘ └───────┘└┘└────┘ ┴└─
pid ───────────────────────────┘ └───────────────┘ └──
st ───────────────────┘└────────────────────────────┘└─
752 exact ⟨_, _, rfl, rfl⟩ } },
id └─┘
src ───────────────┘ └────┘ └┘└─┘└──────
typ ───────────────┘ └────┘ └┘└─┘└──────
doc ───────────────┘ └────┘ └┘ └──────
txt ───────────────┘ └────┘ └┘ └──────
par ───────────────┘ └────┘ └┘ └──────
pid ───────────────┘ └────┘ └┘ └──────
st ────────────────────────────────┘└─┘└─
753 { intros x s, refine ⟨s, S, rfl, rfl⟩ }
id ┴ ┴ └─┘
src ───────┘└────────┘└┘└─────┘ └┘ └┘ └┘└─┘└┘└─
typ ───────┘└────────┘└───────┘ ┴└┘┴└┘ └┘└─┘└───
doc ───────┘└────────┘└┘└─────┘ └┘ └┘ └┘ └┘└─
txt ───────┘└────────┘└┘└─────┘ └┘ └┘ └┘ └┘└─
par ───────┘└────────┘└───────┘ └┘ └┘ └┘ └───
pid ──────────────────────────┘ └┘ └┘ └┘ └───
st ─────────────────┘└────────────────────────┘└─
754 end end },
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ──────────┘┴
st ──────┘└───┘└┘└
755 { refine ⟨nil, S, _, _⟩; simp }
id └─┘ ┴
src └─────┘ └─┘└┘ └─────┘ └───┘
typ └─────┘ └─┘└┘┴└─────┘ └───┘
doc └─────┘ └─┘└┘ └─────┘ └───┘
txt └─────┘ └┘ └─────┘ └───┘
par └─────┘ └┘ └─────┘ └───┘
pid ┴ └┘ └─────┘ ┴
st ───────────────────────────────┘└─
756 end
st ──┘
757
758 @[simp] theorem map_join (f : α → β) : ∀ S, map f (join S) = join (map (map f) S)
id ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ ┴
src └─┘ └──┘ ┴ └──┘ └─┘ └─┘
typ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ ┴
doc └──┘ └─┘ └──┘ └──┘ └─┘ └─┘
759 | ((a, s), S) := by apply cases_on s; intros; simp [map]
id └┘ └──────┘ ┴ └─┘
src └┘ └────┘└──────┘┴ └────┘ └────┘└─┘└─
typ └┘ └────┘└──────┘┴┴ └────┘ └────┘└─┘└─
doc └────┘ ┴ └────┘ └────┘└─┘└─
txt └────┘ ┴ └────┘ └────┘ └─
par └────┘ ┴ └────┘ └────┘ └─
pid ┴ ┴ ┴┴ ┴└
st └─────────────────────────────────────
760
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
761 @[simp] theorem join_join (SS : seq (seq1 (seq1 α))) :
id └─┘ └──┘ └──┘ ┴
src └─┘ └──┘ └──┘
typ └─┘ └──┘ └──┘ ┴
doc └──┘ └─┘ └──┘ └──┘
762 seq.join (seq.join SS) = seq.join (seq.map join SS) :=
id └──────┘ └──────┘ └┘ ┴ └──────┘ └─────┘ └──┘ └┘
src └──────┘ └──────┘ ┴ └──────┘ └─────┘ └──┘
typ └──────┘ └──────┘ └┘ ┴ └──────┘ └─────┘ └──┘ └┘
doc └──────┘ └──────┘ └──────┘ └─────┘ └──┘
763 begin
st └─────
764 apply eq_of_bisim (λs1 s2,
id └─────────┘
src └────┘└─────────┘┴ └──────
typ └────┘└─────────┘┴ └──────
doc └────┘ ┴ └──────
txt └────┘ ┴ └──────
par └────┘ ┴ └──────
pid ┴ ┴ └──────
st ─────────────────────────────
765 ∃ s SS, s1 = seq.append s (seq.join (seq.join SS)) ∧
id ┴ ┴ ┴ ┴
src ───┘┴└───┘┴┴ ┴┴┴ ┴ ┴ ┴ ┴ └─┘┴└
typ ───┘┴└───┘┴┴ ┴┴┴ ┴ ┴ ┴ ┴ └─┘┴└
doc ───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
txt ───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ───┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ─────────────────────────────────────────────────────────
766 s2 = seq.append s (seq.join (seq.map join SS))),
id └────────┘ └──────┘ └─────┘ └──┘
src ─────┘ ┴ ┴└────────┘┴ ┴ └──────┘┴ └─────┘┴└──┘┴ └─┘
typ ─────┘ ┴ ┴└────────┘┴ ┴ └──────┘┴ └─────┘┴└──┘┴ └─┘
doc ─────┘ ┴ ┴└────────┘┴ ┴ └──────┘┴ └─────┘┴└──┘┴ └─┘
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────┘└─
767 { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, SS, rfl, rfl⟩ := begin
id └┘ └┘ ┴ └─┘
src └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘└─┘└───┘ └
typ └────────────┘ └────┘ ┴└┘└┘└┘└┘┴└────┘ └┘ └┘ └┘ └┘ └┘└─┘└───┘ └
doc └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
txt └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
par └────────────┘ └────┘ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
pid └──────┘ ┴ ┴ └┘ └┘ └────┘ └┘ └┘ └┘ └┘ └┘ └───┘ └
st ───┘└────────────┘└────────────────────────────────────────────────────────┘└─────
768 apply cases_on s; simp,
id └──────┘ ┴
src ─────┘└────┘└──────┘┴ └┘└──┘└─
typ ───────────┘└──────┘┴┴└┘└──┘└─
doc ─────┘└────┘ ┴ └┘└──┘└─
txt ─────┘└────┘ ┴ └┘└──┘└─
par ───────────┘ ┴ └┘└──┘└─
pid ───────────┘ ┴ └───────
st ───────────────────────────┘└─
769 { apply cases_on SS; simp,
id └──────┘ └┘
src ───────┘└────┘└──────┘┴ └┘└──┘└─
typ ─────────────┘└──────┘┴└┘└┘└──┘└─
doc ───────┘└────┘ ┴ └┘└──┘└─
txt ───────┘└────┘ ┴ └┘└──┘└─
par ─────────────┘ ┴ └┘└──┘└─
pid ─────────────┘ ┴ └───────
st ──────┘└──────────────────────┘└─
770 { intros S SS, cases S with s S; cases s with x s; simp [map],
id ┴ ┴ └─┘
src ─────────┘└─────────┘└┘└────┘ └───────┘└┘└────┘ └───────┘└┘└────┘└─┘┴└─
typ ─────────┘└─────────┘└┘└────┘┴└───────┘└┘└────┘┴└───────┘└┘└────┘└─┘┴└─
doc ─────────┘└─────────┘└┘└────┘ └───────┘└┘└────┘ └───────┘└┘└────┘└─┘┴└─
txt ─────────┘└─────────┘└┘└────┘ └───────┘└┘└────┘ └───────┘└┘└────┘ ┴└─
par ─────────┘└─────────┘└┘└────┘ └───────┘└┘└────┘ └───────┘└┘└────┘ ┴└─
pid ────────────────────────────┘ └───────────────┘ └───────────────┘ └──
st ────────────────────┘└──────────────────────────────────────────────┘└─
771 apply cases_on s; simp,
id └──────┘ ┴
src ─────────┘└────┘└──────┘┴ └┘└──┘└─
typ ───────────────┘└──────┘┴┴└┘└──┘└─
doc ─────────┘└────┘ ┴ └┘└──┘└─
txt ─────────┘└────┘ ┴ └┘└──┘└─
par ───────────────┘ ┴ └┘└──┘└─
pid ───────────────┘ ┴ └───────
st ───────────────────────────────┘└─
772 { exact ⟨_, _, rfl, rfl⟩ },
id └─┘
src ─────────────────┘ └────┘ └┘└─┘└────
typ ─────────────────┘ └────┘ └┘└─┘└────
doc ─────────────────┘ └────┘ └┘ └────
txt ─────────────────┘ └────┘ └┘ └────
par ─────────────────┘ └────┘ └┘ └────
pid ─────────────────┘ └────┘ └┘ └────
st ──────────┘└──────────────────────┘┴└─
773 { intros x s,
src ───────────┘└────────┘└─
typ ───────────┘└────────┘└─
doc ───────────┘└────────┘└─
txt ───────────┘└────────┘└─
par ───────────┘└────────┘└─
pid ────────────────────────
st ─────────────────────┘└─
774 refine ⟨cons x (append s (seq.join S)), SS, _, _⟩; simp } } },
id └──┘ ┴ └────┘ ┴ └──────┘ ┴ └┘
src ───────────┘└─────┘ └──┘┴ ┴ └────┘┴ ┴ └──────┘┴ └──┘ └─────┘└┘└───┘└──────
typ ──────────────────┘ └──┘┴┴┴ └────┘┴┴┴ └──────┘┴┴└──┘└┘└───────┘└───┘└──────
doc ───────────┘└─────┘ └──┘┴ ┴ └────┘┴ ┴ └──────┘┴ └──┘ └─────┘└┘└───┘└──────
txt ───────────┘└─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─────┘└┘└───┘└──────
par ──────────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───────┘└───┘└──────
pid ──────────────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └────────────────────
st ───────────────────────────────────────────────────────────────────┘└───┘└─
775 { intros x s, exact ⟨s, SS, rfl, rfl⟩ }
id ┴ └┘ └─┘
src ───────┘└────────┘└──────┘ └┘ └┘ └┘└─┘└───
typ ───────┘└────────┘└──────┘ ┴└┘└┘└┘ └┘└─┘└───
doc ───────┘└────────┘└──────┘ └┘ └┘ └┘ └───
txt ───────┘└────────┘└──────┘ └┘ └┘ └┘ └───
par ───────┘└────────┘└──────┘ └┘ └┘ └┘ └───
pid ─────────────────────────┘ └┘ └┘ └┘ └───
st ─────────────────┘└────────────────────────┘└─
776 end end },
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ──────────┘┴
st ──────┘└───┘└┘└
777 { refine ⟨nil, SS, _, _⟩; simp }
id └─┘ └┘
src └─────┘ └─┘└┘ └─────┘ └───┘
typ └─────┘ └─┘└┘└┘└─────┘ └───┘
doc └─────┘ └─┘└┘ └─────┘ └───┘
txt └─────┘ └┘ └─────┘ └───┘
par └─────┘ └┘ └─────┘ └───┘
pid ┴ └┘ └─────┘ ┴
st ────────────────────────────────┘└─
778 end
st ──┘
779
780 @[simp] theorem bind_assoc (s : seq1 α) (f : α → seq1 β) (g : β → seq1 γ) :
id └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘ └──┘
781 bind (bind s f) g = bind s (λ (x : α), bind (f x) g) :=
id └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ └──┘ ┴ └──┘ └──┘
typ └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘ └──┘
782 begin
st └─────
783 cases s with a s,
id ┴
src └────┘ └───────┘
typ └────┘┴└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ─────────────────┘└─
784 simp [bind, map],
id └──┘ └─┘
src └────┘└──┘└┘└─┘┴
typ └────┘└──┘└┘└─┘┴
doc └────┘└──┘└┘└─┘┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ─────────────────┘└─
785 rw [←map_comp],
id └──────┘
src └───┘└──────┘┴
typ └───┘└──────┘┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ──────────────┘└──
786 change (λ x, join (map g (f x))) with (join ∘ ((map g) ∘ f)),
id └──┘ └─┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴
src └─────┘ └──┘└──┘┴ └─┘┴ ┴ ┴ └───────┘ └──┘┴┴┴ └─┘┴ └┘ ┴ └┘
typ └─────┘ └──┘└──┘┴ └─┘┴┴┴ ┴┴ └───────┘ └──┘┴┴┴ └─┘┴┴└┘ ┴┴└┘
doc └─────┘ └──┘└──┘┴ └─┘┴ ┴ ┴ └───────┘ └──┘┴ ┴ └─┘┴ └┘ ┴ └┘
txt └─────┘ └──┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘ ┴ └┘
par └─────┘ └──┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘ ┴ └┘
pid ┴ └──┘ ┴ ┴ ┴ ┴ └─┘└────┘ ┴ ┴ ┴ └┘ ┴ └┘
st ─────────────────────────────────────────────────────────────┘└─
787 rw [map_comp _ join],
id └──────┘ └──┘
src └──┘└──────┘└─┘└──┘┴
typ └──┘└──────┘└─┘└──┘┴
doc └──┘ └─┘└──┘┴
txt └──┘ └─┘ ┴
par └──┘ └─┘ ┴
pid └┘ └─┘ ┴
st ────────────────────┘└──
788 generalize : seq.map (map g ∘ f) s = SS,
id └─────┘ └─┘ ┴ ┴ ┴
src └───────────┘└─────┘┴ └─┘┴ ┴ ┴ └┘ ┴ ┴
typ └───────────┘└─────┘┴ └─┘┴┴┴ ┴┴└┘┴┴ ┴
doc └───────────┘└─────┘┴ └─┘┴ ┴ ┴ └┘ ┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────┘└─
789 rcases map g (f a) with ⟨⟨a, s⟩, S⟩,
id └─┘ ┴ ┴ ┴
src └─────┘└─┘┴ ┴ ┴ └────────────────┘
typ └─────┘└─┘┴┴┴ ┴┴┴└────────────────┘
doc └─────┘└─┘┴ ┴ ┴ └────────────────┘
txt └─────┘ ┴ ┴ ┴ └────────────────┘
par └─────┘ ┴ ┴ ┴ └────────────────┘
pid ┴ ┴ ┴ ┴ └────────────────┘
st ────────────────────────────────────┘└─
790 apply cases_on s; intros; apply cases_on S; intros; simp,
id └──────┘ ┴ └──────┘ ┴
src └────┘└──────┘┴ └────┘ └────┘└──────┘┴ └────┘ └──┘
typ └────┘└──────┘┴┴ └────┘ └────┘└──────┘┴┴ └────┘ └──┘
doc └────┘ ┴ └────┘ └────┘ ┴ └────┘ └──┘
txt └────┘ ┴ └────┘ └────┘ ┴ └────┘ └──┘
par └────┘ ┴ └────┘ └────┘ ┴ └────┘ └──┘
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
791 { cases x with x t, apply cases_on t; intros; simp },
id ┴ └──────┘ ┴
src └────┘ └───────┘ └────┘└──────┘┴ └────┘ └───┘
typ └────┘┴└───────┘ └────┘└──────┘┴┴ └────┘ └───┘
doc └────┘ └───────┘ └────┘ ┴ └────┘ └───┘
txt └────┘ └───────┘ └────┘ ┴ └────┘ └───┘
par └────┘ └───────┘ └────┘ ┴ └────┘ └───┘
pid ┴ └───────┘ ┴ ┴ ┴
st ───┘└──────────────┘└───────────────────────────────┘└┘└
792 { cases x_1 with y t; simp }
id └─┘
src └────┘ └───────┘ └───┘
typ └────┘└─┘└───────┘ └───┘
doc └────┘ └───────┘ └───┘
txt └────┘ └───────┘ └───┘
par └────┘ └───────┘ └───┘
pid ┴ └───────┘ ┴
st ────────────────────────────┘└─
793 end
st ──┘
794
795 instance : monad seq1 :=
id └───┘ └──┘
src └───┘ └──┘
typ └───┘ └──┘
doc └──┘
796 { map := @map,
id └─┘
src └─┘
typ └─┘
doc └─┘
797 pure := @ret,
id └─┘
src └─┘
typ └─┘
doc └─┘
798 bind := @bind }
id └──┘
src └──┘
typ └──┘
doc └──┘
799
800 instance : is_lawful_monad seq1 :=
id └─────────────┘ └──┘
src └─────────────┘ └──┘
typ └─────────────┘ └──┘
doc └──┘
801 { id_map := @map_id,
id ┴ └────┘
src ┴ └────┘
typ ┴ └────┘
802 bind_pure_comp_eq_map := @bind_ret,
id └──────┘
src └──────┘
typ └──────┘
803 pure_bind := @ret_bind,
id └──────┘
src └──────┘
typ └──────┘
804 bind_assoc := @bind_assoc }
id └────────┘
src └────────┘
typ └────────┘
805
806 end seq1